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	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
	elnelneqd.2	⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐵 )
Assertion	elnelneqd	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elnelneqd.1	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
2		elnelneqd.2	⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐵 )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐶 ∈ 𝐴 )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
5	3 4	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐶 ∈ 𝐵 )
6	2 5	mtand	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )