This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elpwgdedVD

Description: Membership in a power class. Theorem 86 of Suppes p. 47. Derived from elpwg . In form of VD deduction with ph and ps as variable virtual hypothesis collections based on Mario Carneiro's metavariable concept. elpwgded is elpwgdedVD using conventional notation. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses elpwgdedVD.1 ⊢ (    𝜑    ▶    𝐴 ∈ V    )
elpwgdedVD.2 ⊢ (    𝜓    ▶    𝐴 ⊆ 𝐵    )
Assertion elpwgdedVD (    (    𝜑    ,    𝜓    )    ▶    𝐴 ∈ 𝒫 𝐵    )

Proof

Step Hyp Ref Expression
1 elpwgdedVD.1 ⊢ (    𝜑    ▶    𝐴 ∈ V    )
2 elpwgdedVD.2 ⊢ (    𝜓    ▶    𝐴 ⊆ 𝐵    )
3 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
4 3 biimpar ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ 𝒫 𝐵 )
5 1 2 4 el12 ⊢ (    (    𝜑    ,    𝜓    )    ▶    𝐴 ∈ 𝒫 𝐵    )