Metamath Proof Explorer


Theorem elpwbi

Description: Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022) (Proof shortened by Steven Nguyen, 16-Sep-2022)

Ref Expression
Hypothesis elpwbi.1 𝐵 ∈ V
Assertion elpwbi ( 𝐴𝐵𝐴 ∈ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 elpwbi.1 𝐵 ∈ V
2 1 elpw2 ( 𝐴 ∈ 𝒫 𝐵𝐴𝐵 )
3 2 bicomi ( 𝐴𝐵𝐴 ∈ 𝒫 𝐵 )