Theorem nelne2 3037

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∈ wcel 2098   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2720  df-clel 2806  df-ne 2938

This theorem is referenced by:  nelelne  3038  elnelne2  3055  elneeldif  3963  elpwdifsn  4797  ac5num  10067  infpssrlem4  10337  fpwwe2lem12  10673  zgt1rpn0n1  13055  cats1un  14711  dprdfadd  19984  dprdcntz2  20002  lbsextlem4  21056  lindff1  21761  hauscmplem  23330  fileln0  23774  zcld  24749  dvcnvlem  25928  ppinprm  27104  chtnprm  27106  footexALT  28542  footexlem1  28543  footexlem2  28544  foot  28546  colperpexlem3  28556  mideulem2  28558  opphllem  28559  opphllem2  28572  lnopp2hpgb  28587  colhp  28594  lmieu  28608  trgcopy  28628  trgcopyeulem  28629  cycpmco2lem1  32868  cycpmco2  32875  cyc3genpmlem  32893  unitnz  32967  fracfld  33019  linds2eq  33121  elrspunsn  33170  mxidlnzr  33205  lindsunlem  33355  fedgmul  33362  extdg1id  33388  ordtconnlem1  33558  esum2dlem  33744  subfacp1lem5  34827  heiborlem6  37322  llnle  39023  lplnle  39045  lhpexle1lem  39512  cdleme18b  39797  cdlemg46  40240  cdlemh  40322  ine1  41906  bcc0  43808  fnchoice  44422  climxrre  45167  stoweidlem43  45460  zneoALTV  47038