Reduce ax-11 usage

[BTernaryTau]

This change is a follow-up to #4485. It revises dftr5, unissb, cotrg, cnvsym, and dffun2 to no longer depend on ax-11. It also adds two new theorems.

alcomw

Weak version of ~ alcom . Uses only Tarski's FOL axiom schemes.

dftr2c

Variant of ~ dftr2 with commuted quantifiers, useful for shortening proofs and avoiding ~ ax-11 .

Changes in axiom usage can be found here: 2cad020

[benjub]

That's very nice: even more ax-11 avoidances than I expected.

As for cotrg and dffun2, I maintain as I wrote in #4485 (comment) that it is their statement that should be changed. This can be done later in another PR and by someone else.

Have you looked at all current usages of alcom to see if they can use alcomw ? (similarly, can be done later by someone else if you haven't completed that part) We may be able to reap even more benefits from alcomw. (Then, there may be germane theorems like (r)alcom* and (r)excom* that could follow the same treatment, but that may be too much trouble for the benefits.)

[BTernaryTau]

I think this change covers every theorem that only depends on ax-11 through alcom, has all of the disjoints needed to make use of alcomw, and isn't in a mathbox.

[icecream17]

impressive amount of ax-11 saves, thanks!