Metamath Proof Explorer

Theorem elfpw

Description: Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion elfpw ⊢ A ∈ 𝒫 B ∩ Fin ↔ A ⊆ B ∧ A ∈ Fin

Proof

Step Hyp Ref Expression
1 elin ⊢ A ∈ 𝒫 B ∩ Fin ↔ A ∈ 𝒫 B ∧ A ∈ Fin
2 elpwg ⊢ A ∈ Fin → A ∈ 𝒫 B ↔ A ⊆ B
3 2 pm5.32ri ⊢ A ∈ 𝒫 B ∧ A ∈ Fin ↔ A ⊆ B ∧ A ∈ Fin
4 1 3 bitri ⊢ A ∈ 𝒫 B ∩ Fin ↔ A ⊆ B ∧ A ∈ Fin