Theorem nelne2 3056

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2143   ≠ wne 2958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-ne 2959

This theorem is used by:  nelelne  3059  elnelne2  3076  elneeldif  3919  elpwdifsn  4757  f1ounsn  7270  ac5num  10025  infpssrlem4  10294  fpwwe2lem12  10631  zgt1rpn0n1  13063  cats1un  14763  dprdfadd  20096  dprdcntz2  20114  lbsextlem4  21294  lindff1  21979  hauscmplem  23572  fileln0  24016  zcld  24980  dvcnvlem  26144  ppinprm  27325  chtnprm  27327  tglnpt4  28937  footexALT  29007  footexlem1  29008  footexlem2  29009  foot  29011  colperpexlem3  29022  mideulem2  29024  opphllem  29025  opphllem2  29038  lnopp2hpgb  29054  colhp  29061  plngrotlem1  29078  plngrotlem2  29079  plngrot  29081  lnssplnglem  29082  lmieu  29102  trgcopy  29124  trgcopyeulem  29125  ragraghl  29158  perpprlng  29209  prlngex  29210  prlngmolem1  29211  prlngmid2  29220  quadcgrprlng  29225  cycpmco2lem1  33455  cycpmco2  33462  cyc3genpmlem  33480  unitnz  33567  fracfld  33638  linds2eq  33703  elrspunsn  33746  mxidlnzr  33759  lindsunlem  34023  fedgmul  34030  extdg1id  34065  2sqr3minply  34179  cos9thpiminplylem2  34182  ordtconnlem1  34323  esum2dlem  34491  subfacp1lem5  35684  mh-inf3f1  37080  heiborlem6  38495  llnle  40320  lplnle  40342  lhpexle1lem  40809  cdleme18b  41094  cdlemg46  41537  cdlemh  41619  ine1  43103  bcc0  45078  fnchoice  45777  climxrre  46492  stoweidlem43  46785  zneoALTV  48462  oppfrcllem  49933  oppfrcl2  49935  eloppf  49939