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

Theorem nelne2 3095
Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
Assertion
Ref Expression
nelne2 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)

Proof of Theorem nelne2
StepHypRef Expression
1 eleq1 2893 . . . 4 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
21biimpcd 241 . . 3 (𝐴𝐶 → (𝐴 = 𝐵𝐵𝐶))
32necon3bd 3012 . 2 (𝐴𝐶 → (¬ 𝐵𝐶𝐴𝐵))
43imp 397 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386   = wceq 1658  wcel 2166  wne 2998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2802
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2817  df-clel 2820  df-ne 2999
This theorem is referenced by:  nelelne  3096  elnelne2  3112  elpwdifsn  4538  ac5num  9171  infpssrlem4  9442  fpwwe2lem13  9778  zgt1rpn0n1  12154  cats1un  13810  dprdfadd  18772  dprdcntz2  18790  lbsextlem4  19521  lindff1  20525  hauscmplem  21579  fileln0  22023  zcld  22985  dvcnvlem  24137  ppinprm  25290  chtnprm  25292  footex  26029  foot  26030  colperpexlem3  26040  mideulem2  26042  opphllem  26043  opphllem2  26056  lnopp2hpgb  26071  colhp  26078  lmieu  26092  trgcopy  26112  trgcopyeulem  26113  ordtconnlem1  30514  esum2dlem  30698  subfacp1lem5  31711  heiborlem6  34156  llnle  35592  lplnle  35614  lhpexle1lem  36081  cdleme18b  36366  cdlemg46  36809  cdlemh  36891  bcc0  39378  fnchoice  40005  climxrre  40776  stoweidlem43  41053  zneoALTV  42409
  Copyright terms: Public domain W3C validator