Theorem nelne2 3023

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ne 2926

This theorem is referenced by:  nelelne  3024  elnelne2  3041  elneeldif  3928  elpwdifsn  4753  f1ounsn  7247  ac5num  9989  infpssrlem4  10259  fpwwe2lem12  10595  zgt1rpn0n1  12994  cats1un  14686  dprdfadd  19952  dprdcntz2  19970  lbsextlem4  21071  lindff1  21729  hauscmplem  23293  fileln0  23737  zcld  24702  dvcnvlem  25880  ppinprm  27062  chtnprm  27064  footexALT  28645  footexlem1  28646  footexlem2  28647  foot  28649  colperpexlem3  28659  mideulem2  28661  opphllem  28662  opphllem2  28675  lnopp2hpgb  28690  colhp  28697  lmieu  28711  trgcopy  28731  trgcopyeulem  28732  cycpmco2lem1  33083  cycpmco2  33090  cyc3genpmlem  33108  unitnz  33190  fracfld  33258  linds2eq  33352  elrspunsn  33400  mxidlnzr  33438  lindsunlem  33620  fedgmul  33627  extdg1id  33661  2sqr3minply  33770  cos9thpiminplylem2  33773  ordtconnlem1  33914  esum2dlem  34082  subfacp1lem5  35171  heiborlem6  37810  llnle  39512  lplnle  39534  lhpexle1lem  40001  cdleme18b  40286  cdlemg46  40729  cdlemh  40811  ine1  42302  bcc0  44329  fnchoice  45023  climxrre  45748  stoweidlem43  46041  zneoALTV  47670  oppfrcllem  49116  oppfrcl2  49118  eloppf  49122