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

Proof

Step Hyp Ref Expression
1 difss A B A
2 ssfi A Fin A B A A B Fin
3 1 2 mpan2 A Fin A B Fin