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	⊢ ( ∀ 𝑧 ∈ 𝑀 𝒫 𝑧 ⊆ 𝑀 → ∀ 𝑧 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-sep	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
2		biimp	⊢ ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
3		simpl	⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → 𝑥 ∈ 𝑧 )
4	2 3	syl6	⊢ ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧 ) )
5	4	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧 ) )
6		velpw	⊢ ( 𝑦 ∈ 𝒫 𝑧 ↔ 𝑦 ⊆ 𝑧 )
7		df-ss	⊢ ( 𝑦 ⊆ 𝑧 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧 ) )
8	6 7	bitr2i	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧 ) ↔ 𝑦 ∈ 𝒫 𝑧 )
9	5 8	sylib	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → 𝑦 ∈ 𝒫 𝑧 )
10		ssel	⊢ ( 𝒫 𝑧 ⊆ 𝑀 → ( 𝑦 ∈ 𝒫 𝑧 → 𝑦 ∈ 𝑀 ) )
11	9 10	syl5	⊢ ( 𝒫 𝑧 ⊆ 𝑀 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → 𝑦 ∈ 𝑀 ) )
12		alral	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
13	11 12	jca2	⊢ ( 𝒫 𝑧 ⊆ 𝑀 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ( 𝑦 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
14	13	eximdv	⊢ ( 𝒫 𝑧 ⊆ 𝑀 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑦 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
15	1 14	mpi	⊢ ( 𝒫 𝑧 ⊆ 𝑀 → ∃ 𝑦 ( 𝑦 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
16		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
17	15 16	sylibr	⊢ ( 𝒫 𝑧 ⊆ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
18	17	ralimi	⊢ ( ∀ 𝑧 ∈ 𝑀 𝒫 𝑧 ⊆ 𝑀 → ∀ 𝑧 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )