Metamath Proof Explorer


Theorem dfon2lem2

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011)

Ref Expression
Assertion dfon2lem2 { 𝑥 ∣ ( 𝑥𝐴𝜑𝜓 ) } ⊆ 𝐴

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝑥𝐴𝜑𝜓 ) → 𝑥𝐴 )
2 1 ss2abi { 𝑥 ∣ ( 𝑥𝐴𝜑𝜓 ) } ⊆ { 𝑥𝑥𝐴 }
3 df-pw 𝒫 𝐴 = { 𝑥𝑥𝐴 }
4 2 3 sseqtrri { 𝑥 ∣ ( 𝑥𝐴𝜑𝜓 ) } ⊆ 𝒫 𝐴
5 sspwuni ( { 𝑥 ∣ ( 𝑥𝐴𝜑𝜓 ) } ⊆ 𝒫 𝐴 { 𝑥 ∣ ( 𝑥𝐴𝜑𝜓 ) } ⊆ 𝐴 )
6 4 5 mpbi { 𝑥 ∣ ( 𝑥𝐴𝜑𝜓 ) } ⊆ 𝐴