Add lemmas, reduce axiom usage

[GinoGiotto]

This PR applies the following changes:

• Add cbvmovw -> use it in proofs of cbveuvw, cbvrmovw.

• Add cbveuvw -> use it in proof of cbvreuvw to avoid ax-10, ax-11, ax-12.

• Add cbvrmovw -> complete the quartet cbvralvw, cbvrexvw, cbvrmovw, cbvreuvw.

• Add rabeq0w -> use it in proofs of frc , frirr to avoid ax-10, ax-11, ax-12 (credits and OLD proof not needed).

• Add ralidmw -> use it in dfwe2 to avoid ax-10, ax-12 (credits and OLD proof not needed).

• Edit proofs of ralsng, rexsng to avoid ax-10, ax-12.

• Edit proofs of ralprg, rexprg to avoid ax-10, ax-12.

• Edit proofs of cbviotavw, cbvriotavw to avoid ax-10, ax-11, ax-12.

Axiom usage here: e64d6fd

[avekens]

It should be added why this proof became longer (because of fewer axioms!?).

[GinoGiotto]

Quoting the PR description:

Add rabeq0w -> use it in proofs of frc , frirr to avoid ax-10, ax-11, ax-12 (credits and OLD proof not needed).

Change of frc proof:

1 frc.1        $e |- B e. _V
2 fri          $p |- ( ( ( B e. _V /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
3 1,2 mpanl1   $p |- ( ( R Fr A /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
4 3 3impb      $p |- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x )
5 rabeq0       $p |- ( { y e. B | y R x } = (/) <-> A. y e. B -. y R x )
6 5 rexbii     $p |- ( E. x e. B { y e. B | y R x } = (/) <-> E. x e. B A. y e. B -. y R x )
7 4,6 sylibr   $p |- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) )

1 frc.1        $e |- B e. _V
2 fri          $p |- ( ( ( B e. _V /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. z e. B -. z R x )
3 1,2 mpanl1   $p |- ( ( R Fr A /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. z e. B -. z R x )
4 3 3impb      $p |- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. z e. B -. z R x )
5 breq1        $p |- ( y = z -> ( y R x <-> z R x ) )
6 5 rabeq0w    $p |- ( { y e. B | y R x } = (/) <-> A. z e. B -. z R x )
7 6 rexbii     $p |- ( E. x e. B { y e. B | y R x } = (/) <-> E. x e. B A. z e. B -. z R x )
8 4,7 sylibr   $p |- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) )

The above edit is considered a "simple replacement", where the general proof idea stays the same, but a theorem is replaced with a weaker version using fewer axioms. It's the same kind of edit done in PR #4203 (comment) where it was accepted that these changes don't need credits and OLD proofs.

[avekens]

What about "$( $j usage 'frc' avoids 'ax-10 , ..." ?

[GinoGiotto]

What about "$( $j usage 'frc' avoids 'ax-10 , ..." ?

Even those are typically not added #4015 #4176 #3984, and for a good reason: most likely there are hundreds if not thousands of these edits, so it’s not practical to include any modification that goes beyond the replacement itself. For reference, reducing ax-13 usage required the proof edit of about 1500 theorems (done with the minimizer).

This PR contains only 3 of these simple replacements, so I have no problem including those tags here, I added them in a new commit 30c6fed.

[avekens]

I am not talking about proofs whose axiom usage is implicitly reduced by reducing the axioms for theorems used in the proof, but about proofs which are explictly modified to reduce the axiom usage, as in this case.

[GinoGiotto]

I am not talking about proofs whose axiom usage is implicitly reduced by reducing the axioms for theorems used in the proof, but about proofs which are explictly modified to reduce the axiom usage, as in this case.

Yes, I know. I am talking about those as well. The total amount of proofs that I edited with the minimizer in a span of 35 PRs have been about 1500. Then, the edit of those 1500 proofs caused ax-13 to be dropped by 31000 theorems considering indirect effects.

[avekens]

I am not talking about proofs whose axiom usage is implicitly reduced by reducing the axioms for theorems used in the proof, but about proofs which are explictly modified to reduce the axiom usage, as in this case.