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

Metamath Proof Explorer

Theorem nelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012) (Proof shortened by Wolf Lammen, 14-May-2023)

		Ref	Expression
	Assertion	nelne2	\|- ( ( A e. C /\ -. B e. C ) -> A =/= B )

Proof

Step	Hyp	Ref	Expression
1		nelneq	\|- ( ( A e. C /\ -. B e. C ) -> -. A = B )
2	1	neqned	\|- ( ( A e. C /\ -. B e. C ) -> A =/= B )