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

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

Proof of Theorem nelne1
StepHypRef Expression
1 eleq2 2868 . . . 4 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
21biimpcd 241 . . 3 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
32necon3bd 2986 . 2 (𝐴𝐵 → (¬ 𝐴𝐶𝐵𝐶))
43imp 396 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385   = wceq 1653  wcel 2157  wne 2972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2793  df-clel 2796  df-ne 2973
This theorem is referenced by:  elnelne1  3085  difsnb  4526  fofinf1o  8484  fin23lem24  9433  fin23lem31  9454  ttukeylem7  9626  npomex  10107  lbspss  19402  islbs3  19477  lbsextlem4  19483  obslbs  20398  hauspwpwf1  22118  ppiltx  25254  tglineneq  25894  lnopp2hpgb  26010  colopp  26016  ex-pss  27812  unelldsys  30736  cntnevol  30806  fin2solem  33883  lshpnelb  35004  osumcllem10N  35985  pexmidlem7N  35996  dochsnkrlem1  37489  rpnnen3lem  38378  lvecpsslmod  43090
  Copyright terms: Public domain W3C validator