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 
|- ( ~P A i^i Fin ) =/= (/)

Proof

Step Hyp Ref Expression
1 0pwfi 
 |-  (/) e. ( ~P A i^i Fin )
2 ne0i 
 |-  ( (/) e. ( ~P A i^i Fin ) -> ( ~P A i^i Fin ) =/= (/) )
3 1 2 ax-mp 
 |-  ( ~P A i^i Fin ) =/= (/)