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

Metamath Proof Explorer

Theorem eldifbd

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif . (Contributed by David Moews, 1-May-2017)

		Ref	Expression
	Hypothesis	eldifbd.1	$⊢ φ \to A \in (B ∖ C)$
	Assertion	eldifbd	$⊢ φ \to \neg A \in C$

Proof

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