Attempt to unbundle ax-7

[Norman Megill]

I have been wondering if it is possible to prove ax-7 starting from the weaker version whose set variables are distinct, just as we are able to prove ax-9 (theorem ax9) from ax9v.

So far I haven't been successful at proving or disproving it.

Some partial results are in my mathbox.  For a description see the text above ax-7v,

    http://us2.metamath.org:88/mpeuni/mmtheorems294.html#mm29357s

Using ~ ax-7v in place of ~ ax-7, I was able to prove

    ax7w1AUX7   |- ( A. x x = y -> ( A. x A. y ph -> A. y A. x ph ) )

(with no $d x y) but was unable to prove

                |- ( -. A. x x = y -> ( A. x A. y ph -> A. y A. x ph ) )

Some special cases of ax-7 that can be proved from ax-7v are

    ax7w2AUX7    |- ( A. x A. y [ y / x ] ph -> A. y A. x [ y / x ] ph )
    ax7w3AUX7    |- ( A. x A. y x = y -> A. y A. x x = y )
    ax7w7AUX7    |- ( A. x A. y -. x = y -> A. y A. x -. x = y )
    ax7wnftAUX7  |- ( A. y F/ x ph -> ( A. x A. y ph -> A. y A. x ph ) )

Some other results:

All of the old (obsolete) axioms whose proof used ax-7 now have proofs
with ax-7v:

    ax12oNEW7 ax9NEW7 ax9oNEW7 ax10NEW7 ax10oNEW7 ax11oNEW7 ax15NEW7 ax16NEW7

Theorem aev (which incidentally bundles 60 cases), has been proved from ax-7v:

    aevNEW7    $d x y  =>  |- ( A. x x = y -> A. z w = v )

but an ax-7v proof of hbae

     |- ( A. x x = y -> A. z A. x x = y )

remains elusive.  Some weaker cases of hbae are proved:

    hba1eAUX7 hbaewAUX7 hbaew2AUX7 hbaew3AUX7 hbaew0AUX7 hbaew4AUX7 hbaew5AUX7

A near-term goal is to reprove more of the *OLD7 theorems from ax-7v and move them up to the *NEW7 section.  The more *NEW7 theorems we have the more likely they will provide a clue.  Currently there are 130 *NEW7s that have been reproved and 90 *OLD7s remaining.

Norm