Theorem ssclaxsep

Description: A class that is closed under subsets models the Axiom of Separation ax-sep . Lemma II.2.4(3) of Kunen2 p. 111.

Note that, to obtain the relativization of an instance of Separation to M , the formula ph would need to be replaced with its relativization to M . However, this new formula is a valid substitution for ph , so this theorem does establish that all instances of Separation hold in M . (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Assertion	ssclaxsep	|- ( A. z e. M ~P z C_ M -> A. z e. M E. y e. M A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-sep	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
2		biimp	|- ( ( x e. y <-> ( x e. z /\ ph ) ) -> ( x e. y -> ( x e. z /\ ph ) ) )
3		simpl	|- ( ( x e. z /\ ph ) -> x e. z )
4	2 3	syl6	|- ( ( x e. y <-> ( x e. z /\ ph ) ) -> ( x e. y -> x e. z ) )
5	4	alimi	|- ( A. x ( x e. y <-> ( x e. z /\ ph ) ) -> A. x ( x e. y -> x e. z ) )
6		velpw	|- ( y e. ~P z <-> y C_ z )
7		df-ss	|- ( y C_ z <-> A. x ( x e. y -> x e. z ) )
8	6 7	bitr2i	|- ( A. x ( x e. y -> x e. z ) <-> y e. ~P z )
9	5 8	sylib	|- ( A. x ( x e. y <-> ( x e. z /\ ph ) ) -> y e. ~P z )
10		ssel	|- ( ~P z C_ M -> ( y e. ~P z -> y e. M ) )
11	9 10	syl5	|- ( ~P z C_ M -> ( A. x ( x e. y <-> ( x e. z /\ ph ) ) -> y e. M ) )
12		alral	|- ( A. x ( x e. y <-> ( x e. z /\ ph ) ) -> A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) )
13	11 12	jca2	|- ( ~P z C_ M -> ( A. x ( x e. y <-> ( x e. z /\ ph ) ) -> ( y e. M /\ A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) ) ) )
14	13	eximdv	|- ( ~P z C_ M -> ( E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) -> E. y ( y e. M /\ A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) ) ) )
15	1 14	mpi	|- ( ~P z C_ M -> E. y ( y e. M /\ A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) ) )
16		df-rex	|- ( E. y e. M A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) <-> E. y ( y e. M /\ A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) ) )
17	15 16	sylibr	|- ( ~P z C_ M -> E. y e. M A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) )
18	17	ralimi	|- ( A. z e. M ~P z C_ M -> A. z e. M E. y e. M A. x e. M ( x e. y <-> ( x e. z /\ ph ) ) )