Metamath Proof Explorer


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 z M 𝒫 z M z M y M x M x y x z φ

Proof

Step Hyp Ref Expression
1 ax-sep y x x y x z φ
2 biimp x y x z φ x y x z φ
3 simpl x z φ x z
4 2 3 syl6 x y x z φ x y x z
5 4 alimi x x y x z φ x x y x z
6 velpw y 𝒫 z y z
7 df-ss y z x x y x z
8 6 7 bitr2i x x y x z y 𝒫 z
9 5 8 sylib x x y x z φ y 𝒫 z
10 ssel 𝒫 z M y 𝒫 z y M
11 9 10 syl5 𝒫 z M x x y x z φ y M
12 alral x x y x z φ x M x y x z φ
13 11 12 jca2 𝒫 z M x x y x z φ y M x M x y x z φ
14 13 eximdv 𝒫 z M y x x y x z φ y y M x M x y x z φ
15 1 14 mpi 𝒫 z M y y M x M x y x z φ
16 df-rex y M x M x y x z φ y y M x M x y x z φ
17 15 16 sylibr 𝒫 z M y M x M x y x z φ
18 17 ralimi z M 𝒫 z M z M y M x M x y x z φ