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

Theorem nelne2 3115
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 2937 . 2 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → ¬ 𝐴 = 𝐵)
21neqned 3023 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2105  wne 3016
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ne 3017
This theorem is referenced by:  nelelne  3117  elnelne2  3134  elneeldif  3949  elpwdifsn  4715  ac5num  9451  infpssrlem4  9717  fpwwe2lem13  10053  zgt1rpn0n1  12420  cats1un  14073  dprdfadd  19073  dprdcntz2  19091  lbsextlem4  19864  lindff1  20894  hauscmplem  21944  fileln0  22388  zcld  23350  dvcnvlem  24502  ppinprm  25657  chtnprm  25659  footexALT  26432  footexlem1  26433  footexlem2  26434  foot  26436  colperpexlem3  26446  mideulem2  26448  opphllem  26449  opphllem2  26462  lnopp2hpgb  26477  colhp  26484  lmieu  26498  trgcopy  26518  trgcopyeulem  26519  cycpmco2lem1  30696  cycpmco2  30703  cyc3genpmlem  30721  linds2eq  30869  lindsunlem  30920  fedgmul  30927  extdg1id  30953  ordtconnlem1  31067  esum2dlem  31251  subfacp1lem5  32329  heiborlem6  34977  llnle  36536  lplnle  36558  lhpexle1lem  37025  cdleme18b  37310  cdlemg46  37753  cdlemh  37835  bcc0  40552  fnchoice  41166  climxrre  41911  stoweidlem43  42209  zneoALTV  43681
  Copyright terms: Public domain W3C validator