Metamath Proof Explorer


Theorem 0pwfi

Description: The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion 0pwfi ∅ ∈ ( 𝒫 𝐴 ∩ Fin )

Proof

Step Hyp Ref Expression
1 0elpw ∅ ∈ 𝒫 𝐴
2 0fin ∅ ∈ Fin
3 1 2 elini ∅ ∈ ( 𝒫 𝐴 ∩ Fin )