This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axrep4OLD

Description: Obsolete version of axrep4 as of 18-Sep-2025. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis axrep4OLD.1 
|- F/ z ph
Assertion axrep4OLD 
|- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 axrep4OLD.1 
 |-  F/ z ph
2 axrep3 
 |-  E. x ( E. z A. y ( ph -> y = z ) -> A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) )
3 2 19.35i 
 |-  ( A. x E. z A. y ( ph -> y = z ) -> E. x A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) )
4 nfv 
 |-  F/ z y e. x
5 nfv 
 |-  F/ z x e. w
6 nfa1 
 |-  F/ z A. z ph
7 5 6 nfan 
 |-  F/ z ( x e. w /\ A. z ph )
8 7 nfex 
 |-  F/ z E. x ( x e. w /\ A. z ph )
9 4 8 nfbi 
 |-  F/ z ( y e. x <-> E. x ( x e. w /\ A. z ph ) )
10 9 nfal 
 |-  F/ z A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) )
11 nfv 
 |-  F/ x y e. z
12 nfe1 
 |-  F/ x E. x ( x e. w /\ ph )
13 11 12 nfbi 
 |-  F/ x ( y e. z <-> E. x ( x e. w /\ ph ) )
14 13 nfal 
 |-  F/ x A. y ( y e. z <-> E. x ( x e. w /\ ph ) )
15 elequ2 
 |-  ( x = z -> ( y e. x <-> y e. z ) )
16 1 19.3 
 |-  ( A. z ph <-> ph )
17 16 anbi2i 
 |-  ( ( x e. w /\ A. z ph ) <-> ( x e. w /\ ph ) )
18 17 exbii 
 |-  ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) )
19 18 a1i 
 |-  ( x = z -> ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) ) )
20 15 19 bibi12d 
 |-  ( x = z -> ( ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) <-> ( y e. z <-> E. x ( x e. w /\ ph ) ) ) )
21 20 albidv 
 |-  ( x = z -> ( A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) <-> A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) )
22 10 14 21 cbvexv1 
 |-  ( E. x A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
23 3 22 sylib 
 |-  ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )