Theorem diffi

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

	Ref	Expression
Assertion	diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		difss	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
2		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ) → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
3	1 2	mpan2	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐵 ) ∈ Fin )