metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

add immediate version of fndm and shorten proofs with it #4028

Closed wlammen closed 4 months ago

wlammen commented 4 months ago

The here introduced immediate version of fndm has 67 applications in Main alone, so I think its addition is justified.

Mathboxes were scanned for its application, too, sometimes fndmd was used.

set.mm shrinks by 21 text lines in total.

delete outdated OLD theorem (not counting in the total above).