Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Conventional Metamath proofs, some derived from VD proofs
elpwgded
Metamath Proof Explorer
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
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ 𝒫 𝐵 )