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

Theorem nelne1 3028
 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 2828 . . . 4 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
21biimpcd 239 . . 3 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
32necon3bd 2946 . 2 (𝐴𝐵 → (¬ 𝐴𝐶𝐵𝐶))
43imp 444 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ≠ wne 2932 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-clel 2756  df-ne 2933 This theorem is referenced by:  elnelne1  3045  difsnb  4482  fofinf1o  8406  fin23lem24  9336  fin23lem31  9357  ttukeylem7  9529  npomex  10010  lbspss  19284  islbs3  19357  lbsextlem4  19363  obslbs  20276  hauspwpwf1  21992  ppiltx  25102  tglineneq  25738  lnopp2hpgb  25854  colopp  25860  ex-pss  27596  unelldsys  30530  cntnevol  30600  fin2solem  33708  lshpnelb  34774  osumcllem10N  35754  pexmidlem7N  35765  dochsnkrlem1  37260  rpnnen3lem  38100  lvecpsslmod  42806
 Copyright terms: Public domain W3C validator