Theorem nelne2 3037

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.)

Assertion

Ref	Expression
nelne2	⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Proof of Theorem nelne2

Step	Hyp	Ref	Expression
1		nelneq 2862	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2944	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2105   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-ne 2938

This theorem is referenced by:  nelelne  3038  elnelne2  3055  elneeldif  3976  elpwdifsn  4793  f1ounsn  7291  ac5num  10073  infpssrlem4  10343  fpwwe2lem12  10679  zgt1rpn0n1  13073  cats1un  14755  dprdfadd  20054  dprdcntz2  20072  lbsextlem4  21180  lindff1  21857  hauscmplem  23429  fileln0  23873  zcld  24848  dvcnvlem  26028  ppinprm  27209  chtnprm  27211  footexALT  28740  footexlem1  28741  footexlem2  28742  foot  28744  colperpexlem3  28754  mideulem2  28756  opphllem  28757  opphllem2  28770  lnopp2hpgb  28785  colhp  28792  lmieu  28806  trgcopy  28826  trgcopyeulem  28827  cycpmco2lem1  33128  cycpmco2  33135  cyc3genpmlem  33153  unitnz  33228  fracfld  33289  linds2eq  33388  elrspunsn  33436  mxidlnzr  33474  lindsunlem  33651  fedgmul  33658  extdg1id  33690  2sqr3minply  33752  ordtconnlem1  33884  esum2dlem  34072  subfacp1lem5  35168  heiborlem6  37802  llnle  39500  lplnle  39522  lhpexle1lem  39989  cdleme18b  40274  cdlemg46  40717  cdlemh  40799  ine1  42327  bcc0  44335  fnchoice  44966  climxrre  45705  stoweidlem43  45998  zneoALTV  47593