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 ) ) )