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 𝒫 A Fin

Proof

Step Hyp Ref Expression
1 0elpw 𝒫 A
2 0fin Fin
3 1 2 elini 𝒫 A Fin