Metamath Proof Explorer


Theorem pwss

Description: Subclass relationship for power class. (Contributed by NM, 21-Jun-2009)

Ref Expression
Assertion pwss ( 𝒫 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 dfss2 ( 𝒫 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴𝑥𝐵 ) )
2 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
3 2 imbi1i ( ( 𝑥 ∈ 𝒫 𝐴𝑥𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
4 3 albii ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴𝑥𝐵 ) ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
5 1 4 bitri ( 𝒫 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )