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 )