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

Theorem nelne1 3039
Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)
Assertion
Ref Expression
nelne1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)

Proof of Theorem nelne1
StepHypRef Expression
1 nelneq2 2866 . 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:  elnelne1  3057  difsnb  4806  fofinf1o  9372  fin23lem24  10362  fin23lem31  10383  ttukeylem7  10555  npomex  11036  lbspss  21081  islbs3  21157  lbsextlem4  21163  obslbs  21750  hauspwpwf1  23995  ppiltx  27220  tglineneq  28652  lnopp2hpgb  28771  colopp  28777  ex-pss  30447  drngidlhash  33462  ssdifidlprm  33486  mxidlmaxv  33496  mxidlprm  33498  drnglidl1ne0  33503  drng0mxidl  33504  qsdrnglem2  33524  rsprprmprmidl  33550  1arithufdlem4  33575  ply1annnr  33746  irngnminplynz  33755  algextdeglem4  33761  unelldsys  34159  cntnevol  34229  fin2solem  37613  lshpnelb  38985  osumcllem10N  39967  pexmidlem7N  39978  dochsnkrlem1  41471  ricdrng1  42538  rpnnen3lem  43043  lvecpsslmod  48424
  Copyright terms: Public domain W3C validator