Theorem nelne2 3028

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

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

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-ne 2931

This theorem is referenced by:  nelelne  3029  elnelne2  3046  elneeldif  3913  elpwdifsn  4743  f1ounsn  7216  ac5num  9944  infpssrlem4  10214  fpwwe2lem12  10551  zgt1rpn0n1  12946  cats1un  14642  dprdfadd  19949  dprdcntz2  19967  lbsextlem4  21114  lindff1  21773  hauscmplem  23348  fileln0  23792  zcld  24756  dvcnvlem  25934  ppinprm  27116  chtnprm  27118  footexALT  28739  footexlem1  28740  footexlem2  28741  foot  28743  colperpexlem3  28753  mideulem2  28755  opphllem  28756  opphllem2  28769  lnopp2hpgb  28784  colhp  28791  lmieu  28805  trgcopy  28825  trgcopyeulem  28826  cycpmco2lem1  33157  cycpmco2  33164  cyc3genpmlem  33182  unitnz  33270  fracfld  33339  linds2eq  33411  elrspunsn  33459  mxidlnzr  33497  lindsunlem  33730  fedgmul  33737  extdg1id  33772  2sqr3minply  33886  cos9thpiminplylem2  33889  ordtconnlem1  34030  esum2dlem  34198  subfacp1lem5  35327  heiborlem6  37956  llnle  39717  lplnle  39739  lhpexle1lem  40206  cdleme18b  40491  cdlemg46  40934  cdlemh  41016  ine1  42511  bcc0  44523  fnchoice  45216  climxrre  45936  stoweidlem43  46229  zneoALTV  47857  oppfrcllem  49314  oppfrcl2  49316  eloppf  49320