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

Metamath Proof Explorer

Theorem elneeldif

Description: The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023)

		Ref	Expression
	Assertion	elneeldif	$⊢ (X \in A \land Y \in (B ∖ A)) \to X \neq Y$

Step	Hyp	Ref	Expression
1		eldif	$⊢ Y \in (B ∖ A) \leftrightarrow (Y \in B \land \neg Y \in A)$
2		nelne2	$⊢ (X \in A \land \neg Y \in A) \to X \neq Y$
3	2	ex	$⊢ X \in A \to (\neg Y \in A \to X \neq Y)$
4	3	adantld	$⊢ X \in A \to ((Y \in B \land \neg Y \in A) \to X \neq Y)$
5	1 4	biimtrid	$⊢ X \in A \to (Y \in (B ∖ A) \to X \neq Y)$
6	5	imp	$⊢ (X \in A \land Y \in (B ∖ A)) \to X \neq Y$