Theorem nelne2 3053

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-ne 2956

This theorem is used by:  nelelne  3056  elnelne2  3073  elneeldif  3913  elpwdifsn  4752  f1ounsn  7274  ac5num  10042  infpssrlem4  10311  fpwwe2lem12  10654  zgt1rpn0n1  13088  cats1un  14793  dprdfadd  20152  dprdcntz2  20170  lbsextlem4  21351  lindff1  22036  hauscmplem  23634  fileln0  24079  zcld  25043  dvcnvlem  26206  ppinprm  27391  chtnprm  27393  tglnpt4  29005  footexALT  29075  footexlem1  29076  footexlem2  29077  foot  29079  colperpexlem3  29090  mideulem2  29092  opphllem  29093  opphllem2  29106  lnopp2hpgb  29123  colhp  29130  plngrotlem1  29147  plngrotlem2  29148  plngrot  29150  lnssplnglem  29151  lmieu  29171  trgcopy  29193  trgcopyeulem  29194  ragraghl  29228  tgaaddcpbllem1  29231  tgaaddcpbl  29234  perpprlng  29310  prlngex  29311  prlngmolem1  29312  prlngmid2  29321  quadcgrprlng  29326  cycpmco2lem1  33569  cycpmco2  33576  cyc3genpmlem  33594  unitnz  33681  fracfld  33752  linds2eq  33817  elrspunsn  33860  mxidlnzr  33873  lindsunlem  34137  fedgmul  34144  extdg1id  34179  2sqr3minply  34293  cos9thpiminplylem2  34296  ordtconnlem1  34437  esum2dlem  34605  subfacp1lem5  35766  heiborlem6  38569  llnle  40394  lplnle  40416  lhpexle1lem  40883  cdleme18b  41168  cdlemg46  41611  cdlemh  41693  ine1  43192  bcc0  45167  fnchoice  45866  climxrre  46581  stoweidlem43  46874  zneoALTV  48588  oppfrcllem  50056  oppfrcl2  50058  eloppf  50062