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

Theorem nelne2 3029
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 2827 . . . 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:  nelelne  3030  elnelne2  3046  elpwdifsn  4465  ac5num  9049  infpssrlem4  9320  fpwwe2lem13  9656  zgt1rpn0n1  12064  cats1un  13675  dprdfadd  18619  dprdcntz2  18637  lbsextlem4  19363  lindff1  20361  hauscmplem  21411  fileln0  21855  zcld  22817  dvcnvlem  23938  ppinprm  25077  chtnprm  25079  footex  25812  foot  25813  colperpexlem3  25823  mideulem2  25825  opphllem  25826  opphllem2  25839  lnopp2hpgb  25854  colhp  25861  lmieu  25875  trgcopy  25895  trgcopyeulem  25896  ordtconnlem1  30279  esum2dlem  30463  subfacp1lem5  31473  heiborlem6  33928  llnle  35307  lplnle  35329  lhpexle1lem  35796  cdleme18b  36082  cdlemg46  36525  cdlemh  36607  bcc0  39041  fnchoice  39687  climxrre  40485  stoweidlem43  40763  zneoALTV  42090
  Copyright terms: Public domain W3C validator