Preparatory theorems 2/2 (#2462)
Preparatory theorems 2/2 (#2462)

* Preparatory theorems 1/2: the 11 elv theorems

I submit my Preparatory theorems in 2 parts: this is the controversial one. I think these 11 theorems are ok in my Mathbox, and they would decrease the size of set.mm with hundreds of theorems with  ` $e |- A e. _V ` , but I’m quite sure I can’t see the playing field completely. I’ll just write here what I do:
When I met with a ` $e |- A e. _V ` , I found the general version and I included only this general version in my Mathbox. I didn’t use the ` g ` suffix at all because the general version is the default form in my Mathbox (of course I used ` d ` and ` f ` versions). In proofs, I used the default general version this way: ` elv.1 $e |- ( x e. _V -> ph ) $. `  ` elv $p |- ph $= ` . Of course, exceptions exist, and
` A ` is not always  ` x ` in proofs (for example, I used inference form ~ elqs with ~ 0ex and not the general form ~ elqsg in my ~ n0elqs in order to minimize it),
and if you need the same ` $e |- x e. _V ` in a proof several times, the proof can be longer,
but I find this approach by and large simpler and more economical.

* blank characters

2 of them.

* Preparatory theorems 2/2

The remaining preparatory theorems (which don't need new definitions).

* Fix external theorem references

Changed references to theorems not yet in my Mathbox from ` ~ ` to ` T ` and now to `T_ `.

* Improvements

bian -> biancom
biand -> biancomd
ineq -> ineqcom
ineqi -> ineqcomi
rabbiia2 -> rabbii
residcp -> idinxpres
relcnveq3 -> relcnveq4
twsymr -> relcnveq3 (I need this)
references nonexisting theorems to the conventional ~~?
br1steqORIG removed
br2ndeqORIG removed
ralid removed (same reason)
opidORIG notes changed (same reason)

* Improvement

minor
metamath/set.mm,metamath/set.mm,metamath/set.mm