Theorem elnelneqd

Description: Two classes are not equal if there is an element of one which is not an element of the other. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	elnelneqd.1	|- ( ph -> C e. A )
	elnelneqd.2	|- ( ph -> -. C e. B )
Assertion	elnelneqd	|- ( ph -> -. A = B )

Proof

Step	Hyp	Ref	Expression
1		elnelneqd.1	|- ( ph -> C e. A )
2		elnelneqd.2	|- ( ph -> -. C e. B )
3	1	adantr	|- ( ( ph /\ A = B ) -> C e. A )
4		simpr	|- ( ( ph /\ A = B ) -> A = B )
5	3 4	eleqtrd	|- ( ( ph /\ A = B ) -> C e. B )
6	2 5	mtand	|- ( ph -> -. A = B )