Theorem diffi

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

	Ref	Expression
Assertion	diffi	$$⊢A\in \mathrm{Fin}\to A\setminus B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢A\setminus B\subseteq A$$
2		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\setminus B\subseteq A\right)\to A\setminus B\in \mathrm{Fin}$$
3	1 2	mpan2	$$⊢A\in \mathrm{Fin}\to A\setminus B\in \mathrm{Fin}$$