Theorem nelne2 3117

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2114   ≠ wne 3018

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-ne 3019

This theorem is referenced by:  nelelne  3119  elnelne2  3136  elneeldif  3952  elpwdifsn  4723  ac5num  9464  infpssrlem4  9730  fpwwe2lem13  10066  zgt1rpn0n1  12433  cats1un  14085  dprdfadd  19144  dprdcntz2  19162  lbsextlem4  19935  lindff1  20966  hauscmplem  22016  fileln0  22460  zcld  23423  dvcnvlem  24575  ppinprm  25731  chtnprm  25733  footexALT  26506  footexlem1  26507  footexlem2  26508  foot  26510  colperpexlem3  26520  mideulem2  26522  opphllem  26523  opphllem2  26536  lnopp2hpgb  26551  colhp  26558  lmieu  26572  trgcopy  26592  trgcopyeulem  26593  cycpmco2lem1  30770  cycpmco2  30777  cyc3genpmlem  30795  linds2eq  30943  mxidlnzr  30978  lindsunlem  31022  fedgmul  31029  extdg1id  31055  ordtconnlem1  31169  esum2dlem  31353  subfacp1lem5  32433  heiborlem6  35096  llnle  36656  lplnle  36678  lhpexle1lem  37145  cdleme18b  37430  cdlemg46  37873  cdlemh  37955  bcc0  40679  fnchoice  41293  climxrre  42038  stoweidlem43  42335  zneoALTV  43841