This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Fin \to A ∖ B \in Fin$

Step	Hyp	Ref	Expression
1		difss	$⊢ A ∖ B \subseteq A$
2		ssfi	$⊢ (A \in Fin \land A ∖ B \subseteq A) \to A ∖ B \in Fin$
3	1 2	mpan2	$⊢ A \in Fin \to A ∖ B \in Fin$