Theorem nelne2 3034

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 2865	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2943	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2121   ≠ wne 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-ne 2937

This theorem is referenced by:  nelelne  3035  elnelne2  3052  elneeldif  3899  elpwdifsn  4725  f1ounsn  7220  ac5num  9953  infpssrlem4  10223  fpwwe2lem12  10560  zgt1rpn0n1  12980  cats1un  14678  dprdfadd  19992  dprdcntz2  20010  lbsextlem4  21158  lindff1  21799  hauscmplem  23393  fileln0  23837  zcld  24801  dvcnvlem  25965  ppinprm  27137  chtnprm  27139  footexALT  28808  footexlem1  28809  footexlem2  28810  foot  28812  colperpexlem3  28822  mideulem2  28824  opphllem  28825  opphllem2  28838  lnopp2hpgb  28853  colhp  28860  lmieu  28874  trgcopy  28894  trgcopyeulem  28895  cycpmco2lem1  33211  cycpmco2  33218  cyc3genpmlem  33236  unitnz  33324  fracfld  33396  linds2eq  33468  elrspunsn  33516  mxidlnzr  33554  lindsunlem  33820  fedgmul  33827  extdg1id  33862  2sqr3minply  33976  cos9thpiminplylem2  33979  ordtconnlem1  34120  esum2dlem  34288  subfacp1lem5  35427  mh-inf3f1  36784  heiborlem6  38198  llnle  40025  lplnle  40047  lhpexle1lem  40514  cdleme18b  40799  cdlemg46  41242  cdlemh  41324  ine1  42806  bcc0  44799  fnchoice  45492  climxrre  46207  stoweidlem43  46500  zneoALTV  48174  oppfrcllem  49631  oppfrcl2  49633  eloppf  49637