Theorem axrep3

Description: Axiom of Replacement slightly strengthened from axrep2 ; w may occur free in ph . (Contributed by NM, 2-Jan-1997) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		nfe1	|- F/ y E. y A. z ( ph -> z = y )
2		nfv	|- F/ y z e. x
3		nfv	|- F/ y x e. w
4		nfa1	|- F/ y A. y ph
5	3 4	nfan	|- F/ y ( x e. w /\ A. y ph )
6	5	nfex	|- F/ y E. x ( x e. w /\ A. y ph )
7	2 6	nfbi	|- F/ y ( z e. x <-> E. x ( x e. w /\ A. y ph ) )
8	7	nfal	|- F/ y A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) )
9	1 8	nfim	|- F/ y ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) )
10	9	nfex	|- F/ y E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) )
11		axreplem	|- ( y = w -> ( E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) ) )
12		axrep2	|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )
13	10 11 12	chvarfv	|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) )