I also removed usage of ax-10, ax-11, ax-12 from opeq1 and opeq2. For these two I did not apply a simple replacement like the revisions above, but I proved them again from scratch. Therefore revision tags and OLD proofs are provided.
All added DV conditions are with dummy variables.
Results of these changes:
Drop ax-10 from 626 theorems.
Drop ax-11 from 520 theorems.
Drop ax-12 from 99 theorems.
Most changes in this PR are of the same kind of https://github.com/metamath/set.mm/pull/3984 and https://github.com/metamath/set.mm/pull/3991. Specifically:
I also removed usage of ax-10, ax-11, ax-12 from opeq1 and opeq2. For these two I did not apply a simple replacement like the revisions above, but I proved them again from scratch. Therefore revision tags and OLD proofs are provided.
All added DV conditions are with dummy variables.
Results of these changes:
Drop ax-10 from 626 theorems. Drop ax-11 from 520 theorems. Drop ax-12 from 99 theorems.
Full axiom usage here: https://github.com/metamath/set.mm/commit/9566445b0271163393c10cc0837c718f8d8c4c8b