metamath / set.mm

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

Reduce axiom usage #4065

Closed GinoGiotto closed 3 months ago

GinoGiotto commented 3 months ago

Edit a few proofs to reduce axiom usage, specifically:

All added dv conditions are with dummy variables.

Result: Drop ax-12 from 345 theorems. Drop ax-11 from 439 theorems. Drop ax-10 from 224 theorems. Drop ax-8 From 3 theorems.

Axiom usage here: https://github.com/metamath/set.mm/commit/271a059d8184be3cdcbd32de685a7e0ce4b61b5c