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

Theorem nelne2 3112
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 2934 . 2 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → ¬ 𝐴 = 𝐵)
21neqned 3020 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2105  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ne 3014
This theorem is referenced by:  nelelne  3114  elnelne2  3131  elneeldif  3947  elpwdifsn  4713  ac5num  9450  infpssrlem4  9716  fpwwe2lem13  10052  zgt1rpn0n1  12418  cats1un  14071  dprdfadd  19071  dprdcntz2  19089  lbsextlem4  19862  lindff1  20892  hauscmplem  21942  fileln0  22386  zcld  23348  dvcnvlem  24500  ppinprm  25656  chtnprm  25658  footexALT  26431  footexlem1  26432  footexlem2  26433  foot  26435  colperpexlem3  26445  mideulem2  26447  opphllem  26448  opphllem2  26461  lnopp2hpgb  26476  colhp  26483  lmieu  26497  trgcopy  26517  trgcopyeulem  26518  cycpmco2lem1  30695  cycpmco2  30702  cyc3genpmlem  30720  linds2eq  30868  lindsunlem  30919  fedgmul  30926  extdg1id  30952  ordtconnlem1  31066  esum2dlem  31250  subfacp1lem5  32328  heiborlem6  34975  llnle  36534  lplnle  36556  lhpexle1lem  37023  cdleme18b  37308  cdlemg46  37751  cdlemh  37833  bcc0  40549  fnchoice  41163  climxrre  41907  stoweidlem43  42205  zneoALTV  43711
  Copyright terms: Public domain W3C validator