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

Metamath Proof Explorer

Theorem eldifd

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	eldifd.1	$⊢ φ \to A \in B$
	eldifd.2	$⊢ φ \to \neg A \in C$
Assertion	eldifd	$⊢ φ \to A \in (B ∖ C)$

Proof

Step	Hyp	Ref	Expression
1		eldifd.1	$⊢ φ \to A \in B$
2		eldifd.2	$⊢ φ \to \neg A \in C$
3		eldif	$⊢ A \in (B ∖ C) \leftrightarrow (A \in B \land \neg A \in C)$
4	1 2 3	sylanbrc	$⊢ φ \to A \in (B ∖ C)$