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

Theorem nelne1 2878
 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 2677 . . . 4 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
21biimpcd 238 . . 3 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
32necon3bd 2796 . 2 (𝐴𝐵 → (¬ 𝐴𝐶𝐵𝐶))
43imp 444 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-ne 2782 This theorem is referenced by:  elnelne1  2893  difsnb  4278  fofinf1o  8126  fin23lem24  9027  fin23lem31  9048  ttukeylem7  9220  npomex  9697  lbspss  18903  islbs3  18976  lbsextlem4  18982  obslbs  19893  hauspwpwf1  21601  ppiltx  24703  tglineneq  25339  lnopp2hpgb  25455  colopp  25461  ex-pss  26677  unelldsys  29548  cntnevol  29618  fin2solem  32565  lshpnelb  33289  osumcllem10N  34269  pexmidlem7N  34280  dochsnkrlem1  35776  rpnnen3lem  36616  lvecpsslmod  42090
 Copyright terms: Public domain W3C validator