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	$$⊢\left(X\in A\wedge Y\in \left(B\setminus A\right)\right)\to X\ne Y$$

Proof

Step	Hyp	Ref	Expression
1		eldif	$$⊢Y\in \left(B\setminus A\right)\leftrightarrow \left(Y\in B\wedge \neg Y\in A\right)$$
2		nelne2	$$⊢\left(X\in A\wedge \neg Y\in A\right)\to X\ne Y$$
3	2	ex	$$⊢X\in A\to \left(\neg Y\in A\to X\ne Y\right)$$
4	3	adantld	$$⊢X\in A\to \left(\left(Y\in B\wedge \neg Y\in A\right)\to X\ne Y\right)$$
5	1 4	syl5bi	$$⊢X\in A\to \left(Y\in \left(B\setminus A\right)\to X\ne Y\right)$$
6	5	imp	$$⊢\left(X\in A\wedge Y\in \left(B\setminus A\right)\right)\to X\ne Y$$