This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Negated equality and membership Negated equality 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 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶 ) → 𝐴 ≠ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
nelneq ⊢ ( ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶 ) → ¬ 𝐴 = 𝐵 )
2
1
neqned ⊢ ( ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶 ) → 𝐴 ≠ 𝐵 )