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 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwbi.1 | ⊢ 𝐵 ∈ V | |
2 | 1 | elpw2 | ⊢ ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) |
3 | 2 | bicomi | ⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵 ) |