Metamath Proof Explorer

Theorem diffi

Description: If A is finite, ( A \ B ) is finite. (Contributed by FL, 3-Aug-2009)

Ref Expression
Assertion diffi 
|- ( A e. Fin -> ( A \ B ) e. Fin )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( A \ B ) C_ A
2 ssfi 
 |-  ( ( A e. Fin /\ ( A \ B ) C_ A ) -> ( A \ B ) e. Fin )
3 1 2 mpan2 
 |-  ( A e. Fin -> ( A \ B ) e. Fin )