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 e. A /\ Y e. ( B \ A ) ) -> X =/= Y )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( Y e. ( B \ A ) <-> ( Y e. B /\ -. Y e. A ) )
2		nelne2	|- ( ( X e. A /\ -. Y e. A ) -> X =/= Y )
3	2	ex	|- ( X e. A -> ( -. Y e. A -> X =/= Y ) )
4	3	adantld	|- ( X e. A -> ( ( Y e. B /\ -. Y e. A ) -> X =/= Y ) )
5	1 4	syl5bi	|- ( X e. A -> ( Y e. ( B \ A ) -> X =/= Y ) )
6	5	imp	|- ( ( X e. A /\ Y e. ( B \ A ) ) -> X =/= Y )