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