Theorem nelne2 3026

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-ne 2929

This theorem is referenced by:  nelelne  3027  elnelne2  3044  elneeldif  3911  elpwdifsn  4738  f1ounsn  7206  ac5num  9927  infpssrlem4  10197  fpwwe2lem12  10533  zgt1rpn0n1  12933  cats1un  14628  dprdfadd  19934  dprdcntz2  19952  lbsextlem4  21098  lindff1  21757  hauscmplem  23321  fileln0  23765  zcld  24729  dvcnvlem  25907  ppinprm  27089  chtnprm  27091  footexALT  28696  footexlem1  28697  footexlem2  28698  foot  28700  colperpexlem3  28710  mideulem2  28712  opphllem  28713  opphllem2  28726  lnopp2hpgb  28741  colhp  28748  lmieu  28762  trgcopy  28782  trgcopyeulem  28783  cycpmco2lem1  33095  cycpmco2  33102  cyc3genpmlem  33120  unitnz  33206  fracfld  33274  linds2eq  33346  elrspunsn  33394  mxidlnzr  33432  lindsunlem  33637  fedgmul  33644  extdg1id  33679  2sqr3minply  33793  cos9thpiminplylem2  33796  ordtconnlem1  33937  esum2dlem  34105  subfacp1lem5  35228  heiborlem6  37855  llnle  39616  lplnle  39638  lhpexle1lem  40105  cdleme18b  40390  cdlemg46  40833  cdlemh  40915  ine1  42406  bcc0  44432  fnchoice  45125  climxrre  45847  stoweidlem43  46140  zneoALTV  47768  oppfrcllem  49227  oppfrcl2  49229  eloppf  49233