Metamath Proof Explorer


Theorem wfaxsep

Description: The class of well-founded sets models the Axiom of Separation ax-sep . Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in ph are relativized to W . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)

Ref Expression
Hypothesis wfax.1 W = R1 On
Assertion wfaxsep z W y W x W x y x z φ

Proof

Step Hyp Ref Expression
1 wfax.1 W = R1 On
2 ssclaxsep z W 𝒫 z W z W y W x W x y x z φ
3 pwwf z R1 On 𝒫 z R1 On
4 r1elssi 𝒫 z R1 On 𝒫 z R1 On
5 3 4 sylbi z R1 On 𝒫 z R1 On
6 1 eleq2i z W z R1 On
7 1 sseq2i 𝒫 z W 𝒫 z R1 On
8 5 6 7 3imtr4i z W 𝒫 z W
9 2 8 mprg z W y W x W x y x z φ