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

Theorem nelne2 3040
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 2865 . 2 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → ¬ 𝐴 = 𝐵)
21neqned 2947 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wcel 2108  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-ne 2941
This theorem is referenced by:  nelelne  3041  elnelne2  3058  elneeldif  3965  elpwdifsn  4789  f1ounsn  7292  ac5num  10076  infpssrlem4  10346  fpwwe2lem12  10682  zgt1rpn0n1  13076  cats1un  14759  dprdfadd  20040  dprdcntz2  20058  lbsextlem4  21163  lindff1  21840  hauscmplem  23414  fileln0  23858  zcld  24835  dvcnvlem  26014  ppinprm  27195  chtnprm  27197  footexALT  28726  footexlem1  28727  footexlem2  28728  foot  28730  colperpexlem3  28740  mideulem2  28742  opphllem  28743  opphllem2  28756  lnopp2hpgb  28771  colhp  28778  lmieu  28792  trgcopy  28812  trgcopyeulem  28813  cycpmco2lem1  33146  cycpmco2  33153  cyc3genpmlem  33171  unitnz  33243  fracfld  33310  linds2eq  33409  elrspunsn  33457  mxidlnzr  33495  lindsunlem  33675  fedgmul  33682  extdg1id  33716  2sqr3minply  33791  ordtconnlem1  33923  esum2dlem  34093  subfacp1lem5  35189  heiborlem6  37823  llnle  39520  lplnle  39542  lhpexle1lem  40009  cdleme18b  40294  cdlemg46  40737  cdlemh  40819  ine1  42349  bcc0  44359  fnchoice  45034  climxrre  45765  stoweidlem43  46058  zneoALTV  47656
  Copyright terms: Public domain W3C validator