Metamath Proof Explorer


Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994)

Ref Expression
Hypothesis axrep4.1
|- F/ z ph
Assertion axrep4
|- ( 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 axrep4.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 ) ) )