Metamath Proof Explorer

Theorem elpw2g

Description: Membership in a power class. Theorem 86 of Suppes p. 47. (Contributed by NM, 7-Aug-2000)

Ref Expression
Assertion elpw2g ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elpwi ⊢ ( 𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵 )
2 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
3 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
4 3 biimparc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V ) → 𝐴 ∈ 𝒫 𝐵 )
5 2 4 syldan ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝒫 𝐵 )
6 5 expcom ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵 ) )
7 1 6 impbid2 ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )