Metamath Proof Explorer

Theorem zfcndrep

Description: Axiom of Replacement ax-rep , reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfe1 
 |-  F/ y E. y A. z ( A. y ph -> z = y )
2 nfv 
 |-  F/ y z e. w
3 nfv 
 |-  F/ y w e. x
4 nfa1 
 |-  F/ y A. y A. y ph
5 3 4 nfan 
 |-  F/ y ( w e. x /\ A. y A. y ph )
6 5 nfex 
 |-  F/ y E. w ( w e. x /\ A. y A. y ph )
7 2 6 nfbi 
 |-  F/ y ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) )
8 7 nfal 
 |-  F/ y A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) )
9 1 8 nfim 
 |-  F/ y ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) )
10 9 nfex 
 |-  F/ y E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) )
11 elequ2 
 |-  ( y = x -> ( w e. y <-> w e. x ) )
12 11 anbi1d 
 |-  ( y = x -> ( ( w e. y /\ A. y A. y ph ) <-> ( w e. x /\ A. y A. y ph ) ) )
13 12 exbidv 
 |-  ( y = x -> ( E. w ( w e. y /\ A. y A. y ph ) <-> E. w ( w e. x /\ A. y A. y ph ) ) )
14 13 bibi2d 
 |-  ( y = x -> ( ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) <-> ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) )
15 14 albidv 
 |-  ( y = x -> ( A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) <-> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) )
16 15 imbi2d 
 |-  ( y = x -> ( ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) <-> ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) ) )
17 16 exbidv 
 |-  ( y = x -> ( E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) <-> E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) ) )
18 axrepnd 
 |-  E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) )
19 19.3v 
 |-  ( A. y z e. w <-> z e. w )
20 19.3v 
 |-  ( A. z w e. y <-> w e. y )
21 20 anbi1i 
 |-  ( ( A. z w e. y /\ A. y A. y ph ) <-> ( w e. y /\ A. y A. y ph ) )
22 21 exbii 
 |-  ( E. w ( A. z w e. y /\ A. y A. y ph ) <-> E. w ( w e. y /\ A. y A. y ph ) )
23 19 22 bibi12i 
 |-  ( ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) <-> ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) )
24 23 albii 
 |-  ( A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) <-> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) )
25 24 imbi2i 
 |-  ( ( E. y A. z ( A. y ph -> z = y ) -> A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) ) <-> ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) )
26 25 exbii 
 |-  ( E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) ) <-> E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) )
27 18 26 mpbi 
 |-  E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) )
28 10 17 27 chvar 
 |-  E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) )
29 28 19.35i 
 |-  ( A. w E. y A. z ( A. y ph -> z = y ) -> E. w A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) )
30 nfv 
 |-  F/ w z e. y
31 nfe1 
 |-  F/ w E. w ( w e. x /\ A. y ph )
32 30 31 nfbi 
 |-  F/ w ( z e. y <-> E. w ( w e. x /\ A. y ph ) )
33 32 nfal 
 |-  F/ w A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) )
34 elequ2 
 |-  ( w = y -> ( z e. w <-> z e. y ) )
35 nfa1 
 |-  F/ y A. y ph
36 35 19.3 
 |-  ( A. y A. y ph <-> A. y ph )
37 36 anbi2i 
 |-  ( ( w e. x /\ A. y A. y ph ) <-> ( w e. x /\ A. y ph ) )
38 37 exbii 
 |-  ( E. w ( w e. x /\ A. y A. y ph ) <-> E. w ( w e. x /\ A. y ph ) )
39 38 a1i 
 |-  ( w = y -> ( E. w ( w e. x /\ A. y A. y ph ) <-> E. w ( w e. x /\ A. y ph ) ) )
40 34 39 bibi12d 
 |-  ( w = y -> ( ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) <-> ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) )
41 40 albidv 
 |-  ( w = y -> ( A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) )
42 8 33 41 cbvexv1 
 |-  ( E. w A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
43 29 42 sylib 
 |-  ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )