Theorem wfaxrep

Description: The class of well-founded sets models the Axiom of Replacement ax-rep . Actually, our statement is stronger, since it is an instance of Replacement only when all quantifiers in A. y ph are relativized to W . Essentially part of Corollary II.2.5 of Kunen2 p. 112, but note that our Replacement is different from Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypothesis	wfax.1	|- W = U. ( R1 " On )
Assertion	wfaxrep	|- A. x e. W ( A. w e. W E. y e. W A. z e. W ( A. y ph -> z = y ) -> E. y e. W A. z e. W ( z e. y <-> E. w e. W ( w e. x /\ A. y ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfax.1	|- W = U. ( R1 " On )
2		trwf	|- Tr U. ( R1 " On )
3		treq	|- ( W = U. ( R1 " On ) -> ( Tr W <-> Tr U. ( R1 " On ) ) )
4	2 3	mpbiri	|- ( W = U. ( R1 " On ) -> Tr W )
5		vex	|- f e. _V
6	5	rnex	|- ran f e. _V
7	6	r1elss	|- ( ran f e. U. ( R1 " On ) <-> ran f C_ U. ( R1 " On ) )
8	7	biimpri	|- ( ran f C_ U. ( R1 " On ) -> ran f e. U. ( R1 " On ) )
9	1	sseq2i	|- ( ran f C_ W <-> ran f C_ U. ( R1 " On ) )
10	1	eleq2i	|- ( ran f e. W <-> ran f e. U. ( R1 " On ) )
11	8 9 10	3imtr4i	|- ( ran f C_ W -> ran f e. W )
12	11	3ad2ant3	|- ( ( Fun f /\ dom f e. W /\ ran f C_ W ) -> ran f e. W )
13	12	ax-gen	|- A. f ( ( Fun f /\ dom f e. W /\ ran f C_ W ) -> ran f e. W )
14	13	a1i	|- ( W = U. ( R1 " On ) -> A. f ( ( Fun f /\ dom f e. W /\ ran f C_ W ) -> ran f e. W ) )
15		onwf	|- On C_ U. ( R1 " On )
16		0elon	|- (/) e. On
17	15 16	sselii	|- (/) e. U. ( R1 " On )
18		eleq2	|- ( W = U. ( R1 " On ) -> ( (/) e. W <-> (/) e. U. ( R1 " On ) ) )
19	17 18	mpbiri	|- ( W = U. ( R1 " On ) -> (/) e. W )
20	4 14 19	modelaxrep	|- ( W = U. ( R1 " On ) -> A. x e. W ( A. w e. W E. y e. W A. z e. W ( A. y ph -> z = y ) -> E. y e. W A. z e. W ( z e. y <-> E. w e. W ( w e. x /\ A. y ph ) ) ) )
21	1 20	ax-mp	|- A. x e. W ( A. w e. W E. y e. W A. z e. W ( A. y ph -> z = y ) -> E. y e. W A. z e. W ( z e. y <-> E. w e. W ( w e. x /\ A. y ph ) ) )