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 |
| 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 |