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 2859 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
21neqned 2947 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-ne 2941
This theorem is referenced by:  elnelne1  3056  difsnb  4767  fofinf1o  9274  fin23lem24  10263  fin23lem31  10284  ttukeylem7  10456  npomex  10937  lbspss  20558  islbs3  20632  lbsextlem4  20638  obslbs  21152  hauspwpwf1  23354  ppiltx  26542  tglineneq  27628  lnopp2hpgb  27747  colopp  27753  ex-pss  29414  mxidlprm  32285  unelldsys  32814  cntnevol  32884  fin2solem  36110  lshpnelb  37492  osumcllem10N  38474  pexmidlem7N  38485  dochsnkrlem1  39978  ricdrng1  40762  rpnnen3lem  41398  lvecpsslmod  46674
  Copyright terms: Public domain W3C validator