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

Theorem nelne2 3039
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 2858 . 2 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → ¬ 𝐴 = 𝐵)
21neqned 2947 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-ne 2941
This theorem is referenced by:  nelelne  3040  elnelne2  3057  elneeldif  3925  elpwdifsn  4750  ac5num  9977  infpssrlem4  10247  fpwwe2lem12  10583  zgt1rpn0n1  12961  cats1un  14615  dprdfadd  19804  dprdcntz2  19822  lbsextlem4  20638  lindff1  21242  hauscmplem  22773  fileln0  23217  zcld  24192  dvcnvlem  25356  ppinprm  26517  chtnprm  26519  footexALT  27702  footexlem1  27703  footexlem2  27704  foot  27706  colperpexlem3  27716  mideulem2  27718  opphllem  27719  opphllem2  27732  lnopp2hpgb  27747  colhp  27754  lmieu  27768  trgcopy  27788  trgcopyeulem  27789  cycpmco2lem1  32024  cycpmco2  32031  cyc3genpmlem  32049  linds2eq  32216  mxidlnzr  32284  lindsunlem  32376  fedgmul  32383  extdg1id  32409  ordtconnlem1  32562  esum2dlem  32748  subfacp1lem5  33835  heiborlem6  36321  llnle  38027  lplnle  38049  lhpexle1lem  38516  cdleme18b  38801  cdlemg46  39244  cdlemh  39326  bcc0  42708  fnchoice  43322  climxrre  44077  stoweidlem43  44370  zneoALTV  45947
  Copyright terms: Public domain W3C validator