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

Theorem nelne1 3038
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 2857 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
21neqned 2946 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2106  wne 2939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-ne 2940
This theorem is referenced by:  elnelne1  3056  difsnb  4802  fofinf1o  9310  fin23lem24  10299  fin23lem31  10320  ttukeylem7  10492  npomex  10973  lbspss  20642  islbs3  20717  lbsextlem4  20723  obslbs  21218  hauspwpwf1  23420  ppiltx  26608  tglineneq  27760  lnopp2hpgb  27879  colopp  27885  ex-pss  29546  mxidlmaxv  32433  mxidlprm  32435  qsdrnglem2  32454  unelldsys  32985  cntnevol  33055  fin2solem  36276  lshpnelb  37657  osumcllem10N  38639  pexmidlem7N  38650  dochsnkrlem1  40143  ricdrng1  40904  rpnnen3lem  41539  lvecpsslmod  46834
  Copyright terms: Public domain W3C validator