Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994) (Proof shortened by Matthew House, 18-Sep-2025)

	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		ax-rep	|- ( A. x E. z A. y ( A. z ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) )
3	1	19.3	|- ( A. z ph <-> ph )
4	3	imbi1i	|- ( ( A. z ph -> y = z ) <-> ( ph -> y = z ) )
5	4	albii	|- ( A. y ( A. z ph -> y = z ) <-> A. y ( ph -> y = z ) )
6	5	exbii	|- ( E. z A. y ( A. z ph -> y = z ) <-> E. z A. y ( ph -> y = z ) )
7	6	albii	|- ( A. x E. z A. y ( A. z ph -> y = z ) <-> A. x E. z A. y ( ph -> y = z ) )
8	3	anbi2i	|- ( ( x e. w /\ A. z ph ) <-> ( x e. w /\ ph ) )
9	8	exbii	|- ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) )
10	9	bibi2i	|- ( ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> ( y e. z <-> E. x ( x e. w /\ ph ) ) )
11	10	albii	|- ( A. y ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
12	11	exbii	|- ( E. z A. y ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
13	2 7 12	3imtr3i	|- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )