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

Theorem nelne1 2874
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 2673 . . . 4 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
21biimpcd 237 . . 3 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
32necon3bd 2792 . 2 (𝐴𝐵 → (¬ 𝐴𝐶𝐵𝐶))
43imp 443 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1976  wne 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2599  df-clel 2602  df-ne 2778
This theorem is referenced by:  elnelne1  2889  difsnb  4274  fofinf1o  8100  fin23lem24  9001  fin23lem31  9022  ttukeylem7  9194  npomex  9671  lbspss  18846  islbs3  18919  lbsextlem4  18925  obslbs  19832  hauspwpwf1  21540  ppiltx  24617  tglineneq  25254  lnopp2hpgb  25370  colopp  25376  ex-pss  26440  unelldsys  29351  cntnevol  29421  fin2solem  32365  lshpnelb  33089  osumcllem10N  34069  pexmidlem7N  34080  dochsnkrlem1  35576  rpnnen3lem  36416  lvecpsslmod  42089
  Copyright terms: Public domain W3C validator