metamath / set.mm

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

Remove a few axiom dependencies #4008

Closed GinoGiotto closed 3 months ago

GinoGiotto commented 3 months ago

This PR contains the following proof revisions:

All added DV conditions are with dummy variables, so the strength of the statements is not affected.

wlammen commented 3 months ago

I checked by the theorem lists that no extra axiom was introduced.