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	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵 )