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

Metamath Proof Explorer

Theorem nelelne

Description: Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010) (Proof shortened by AV, 10-May-2020)

		Ref	Expression
	Assertion	nelelne	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nelne2	⊢ ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵 ) → 𝐶 ≠ 𝐴 )
2	1	expcom	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐴 ) )