Theorem zfrep6

Description: A version of the Axiom of Replacement. Normally ph would have free variables x and y . Axiom 6 of Kunen p. 12. The Separation Scheme ax-sep cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep . (Contributed by NM, 10-Oct-2003) Shorten proof and reduce axiom dependencies. (Revised by BJ, 5-Apr-2026)

	Ref	Expression
Assertion	zfrep6	|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )

Proof

Step	Hyp	Ref	Expression
1		euex	|- ( E! y ph -> E. y ph )
2	1	ralimi	|- ( A. x e. z E! y ph -> A. x e. z E. y ph )
3		df-ral	|- ( A. x e. z E! y ph <-> A. x ( x e. z -> E! y ph ) )
4		eumo	|- ( E! y ph -> E* y ph )
5	4	imim2i	|- ( ( x e. z -> E! y ph ) -> ( x e. z -> E* y ph ) )
6		moanimv	|- ( E* y ( x e. z /\ ph ) <-> ( x e. z -> E* y ph ) )
7	5 6	sylibr	|- ( ( x e. z -> E! y ph ) -> E* y ( x e. z /\ ph ) )
8	7	alimi	|- ( A. x ( x e. z -> E! y ph ) -> A. x E* y ( x e. z /\ ph ) )
9	3 8	sylbi	|- ( A. x e. z E! y ph -> A. x E* y ( x e. z /\ ph ) )
10		axrep6	|- ( A. x E* y ( x e. z /\ ph ) -> E. w A. y ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) )
11		rexanid	|- ( E. x e. z ( x e. z /\ ph ) <-> E. x e. z ph )
12	11	bibi2i	|- ( ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) <-> ( y e. w <-> E. x e. z ph ) )
13	12	albii	|- ( A. y ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) <-> A. y ( y e. w <-> E. x e. z ph ) )
14	13	exbii	|- ( E. w A. y ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) <-> E. w A. y ( y e. w <-> E. x e. z ph ) )
15	10 14	sylib	|- ( A. x E* y ( x e. z /\ ph ) -> E. w A. y ( y e. w <-> E. x e. z ph ) )
16	9 15	syl	|- ( A. x e. z E! y ph -> E. w A. y ( y e. w <-> E. x e. z ph ) )
17		replem	|- ( ( A. x e. z E. y ph /\ E. w A. y ( y e. w <-> E. x e. z ph ) ) -> E. w A. x e. z E. y e. w ph )
18	2 16 17	syl2anc	|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )