Metamath Proof Explorer


Theorem pwfin0

Description: A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion pwfin0 ( 𝒫 𝐴 ∩ Fin ) ≠ ∅

Proof

Step Hyp Ref Expression
1 0pwfi ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
2 ne0i ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ )
3 1 2 ax-mp ( 𝒫 𝐴 ∩ Fin ) ≠ ∅