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

Theorem nelne1 3047
 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 2877 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
21neqned 2958 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111   ≠ wne 2951 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830  df-ne 2952 This theorem is referenced by:  elnelne1  3065  difsnb  4696  fofinf1o  8832  fin23lem24  9782  fin23lem31  9803  ttukeylem7  9975  npomex  10456  lbspss  19922  islbs3  19995  lbsextlem4  20001  obslbs  20495  hauspwpwf1  22687  ppiltx  25861  tglineneq  26537  lnopp2hpgb  26656  colopp  26662  ex-pss  28312  mxidlprm  31161  unelldsys  31645  cntnevol  31715  fin2solem  35323  lshpnelb  36560  osumcllem10N  37541  pexmidlem7N  37552  dochsnkrlem1  39045  rpnnen3lem  40345  lvecpsslmod  45281
 Copyright terms: Public domain W3C validator