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

Theorem nelne1 3117
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 2942 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
21neqned 3027 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2107  wne 3020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818  df-clel 2897  df-ne 3021
This theorem is referenced by:  elnelne1  3137  difsnb  4737  fofinf1o  8791  fin23lem24  9736  fin23lem31  9757  ttukeylem7  9929  npomex  10410  lbspss  19776  islbs3  19849  lbsextlem4  19855  obslbs  20790  hauspwpwf1  22511  ppiltx  25668  tglineneq  26344  lnopp2hpgb  26463  colopp  26469  ex-pss  28121  unelldsys  31303  cntnevol  31373  fin2solem  34745  lshpnelb  35987  osumcllem10N  36968  pexmidlem7N  36979  dochsnkrlem1  38472  rpnnen3lem  39489  lvecpsslmod  44390
  Copyright terms: Public domain W3C validator