Metamath Proof Explorer


Theorem elpwgded

Description: elpwgdedVD in conventional notation. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses elpwgded.1 ( 𝜑𝐴 ∈ V )
elpwgded.2 ( 𝜓𝐴𝐵 )
Assertion elpwgded ( ( 𝜑𝜓 ) → 𝐴 ∈ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 elpwgded.1 ( 𝜑𝐴 ∈ V )
2 elpwgded.2 ( 𝜓𝐴𝐵 )
3 elpwg ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝐵𝐴𝐵 ) )
4 3 biimpar ( ( 𝐴 ∈ V ∧ 𝐴𝐵 ) → 𝐴 ∈ 𝒫 𝐵 )
5 1 2 4 syl2an ( ( 𝜑𝜓 ) → 𝐴 ∈ 𝒫 𝐵 )