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

Theorem nelne2 3027
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 2825 . . . 4 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
21biimpcd 239 . . 3 (𝐴𝐶 → (𝐴 = 𝐵𝐵𝐶))
32necon3bd 2944 . 2 (𝐴𝐶 → (¬ 𝐵𝐶𝐴𝐵))
43imp 444 1 ((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1630  wcel 2137  wne 2930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1852  df-cleq 2751  df-clel 2754  df-ne 2931
This theorem is referenced by:  nelelne  3028  elnelne2  3044  elpwdifsn  4463  ac5num  9047  infpssrlem4  9318  fpwwe2lem13  9654  zgt1rpn0n1  12062  cats1un  13673  dprdfadd  18617  dprdcntz2  18635  lbsextlem4  19361  lindff1  20359  hauscmplem  21409  fileln0  21853  zcld  22815  dvcnvlem  23936  ppinprm  25075  chtnprm  25077  footex  25810  foot  25811  colperpexlem3  25821  mideulem2  25823  opphllem  25824  opphllem2  25837  lnopp2hpgb  25852  colhp  25859  lmieu  25873  trgcopy  25893  trgcopyeulem  25894  ordtconnlem1  30277  esum2dlem  30461  subfacp1lem5  31471  heiborlem6  33926  llnle  35305  lplnle  35327  lhpexle1lem  35794  cdleme18b  36080  cdlemg46  36523  cdlemh  36605  bcc0  39039  fnchoice  39685  climxrre  40483  stoweidlem43  40761  zneoALTV  42088
  Copyright terms: Public domain W3C validator