MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nelne2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 nelneq 2853 . 2 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → ¬ 𝐴 = 𝐵)
21neqned 2944 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator