MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elimel Unicode version

Theorem elimel 3630
Description: Eliminate a membership hypothesis for weak deduction theorem, when special case  B  e.  C is provable. (Contributed by NM, 15-May-1999.)
Hypothesis
Ref Expression
elimel.1  |-  B  e.  C
Assertion
Ref Expression
elimel  |-  if ( A  e.  C ,  A ,  B )  e.  C

Proof of Theorem elimel
StepHypRef Expression
1 eleq1 2356 . 2  |-  ( A  =  if ( A  e.  C ,  A ,  B )  ->  ( A  e.  C  <->  if ( A  e.  C ,  A ,  B )  e.  C ) )
2 eleq1 2356 . 2  |-  ( B  =  if ( A  e.  C ,  A ,  B )  ->  ( B  e.  C  <->  if ( A  e.  C ,  A ,  B )  e.  C ) )
3 elimel.1 . 2  |-  B  e.  C
41, 2, 3elimhyp 3626 1  |-  if ( A  e.  C ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   ifcif 3578
This theorem is referenced by:  orduninsuc  4650  oawordeu  6569  oeoa  6611  omopth  6672  unfilem3  7139  inar1  8413  supsr  8750  renegcl  9126  peano5uzti  10117  eluzadd  10272  eluzsub  10273  ltweuz  11040  uzenom  11043  seqfn  11074  seq1  11075  seqp1  11077  sqeqor  11233  binom2  11234  nn0opth2  11303  faclbnd4lem2  11323  hashxp  11402  dvdsle  12590  divalglem7  12614  divalg  12618  gcdaddm  12724  iblcnlem  19159  elimnv  21268  elimnvu  21269  nmlno0i  21388  nmblolbi  21394  blocn  21401  elimphu  21415  ubth  21468  htth  21514  hvsubsub4  21655  hvnegdi  21662  hvsubeq0  21663  hvaddcan  21665  hvsubadd  21672  normlem6  21710  normlem9at  21716  normsq  21729  normsub0  21731  norm-ii  21733  norm-iii  21735  normsub  21738  normpyth  21740  norm3dif  21745  norm3lemt  21747  norm3adifi  21748  normpar  21750  polid  21754  bcs  21776  hhssablo  21856  hhssnvt  21858  shscl  21913  shslej  21975  shincl  21976  pjhth  21988  omlsii  21998  ococ  22001  pjoc1  22029  pjoml  22031  pjoc2  22034  chm0  22086  chne0  22089  chocin  22090  chj0  22092  chincl  22094  chsscon3  22095  chlejb1  22107  chnle  22109  chjo  22110  chdmm1  22120  chjass  22128  ledi  22135  h1de2ci  22151  spansn  22154  elspansn  22161  elspansn2  22162  h1datom  22177  cmbr3  22203  pjoml2  22206  pjoml3  22207  cmcm  22209  cmcm3  22210  lecm  22212  osum  22240  spansnj  22242  spansncv  22248  pjch1  22265  pjadji  22280  pjaddi  22281  pjinormi  22282  pjsubi  22283  pjmuli  22284  pjige0  22286  pjcjt2  22287  pjch  22289  pjhfo  22301  pj11  22309  pjopyth  22315  pjnorm  22319  pjpyth  22320  pjnel  22321  eigre  22431  eigorth  22434  hoddi  22586  nmlnop0  22594  lnopeq0lem2  22602  lnopeq  22605  lnopunilem2  22607  lnopunii  22608  lnophmi  22614  nmbdoplb  22621  nmcopex  22625  nmcoplb  22626  lnopcon  22631  lnfn0  22643  lnfnmul  22644  nmcfnex  22649  nmcfnlb  22650  lnfncon  22652  riesz4  22660  riesz1  22661  cnlnadjeu  22674  pjhmop  22746  pjss2coi  22760  pjssmi  22761  pjssge0i  22762  pjdifnormi  22763  pjidmco  22777  mdslmd1lem3  22923  mdslmd1lem4  22924  csmdsymi  22930  cvmd  22932  hatomic  22956  chrelat2  22966  cvexch  22970  atord  22984  atcvat2  22985  mdsym  23008  kur14  23762  abs2sqle  24031  abs2sqlt  24032  ax5seglem8  24636  onsuccon  24949  onsucsuccmp  24955  alexeqd  25065  ac5g  25178  snelpwg  25194  ab2rexexg  25225  fprg  25236  hmeogrp  25640  cnegvex2b  25765  rnegvex2b  25766  ishomd  25893  selsubf3g  26095  sdclem1  26556  bnj941  29120  bnj944  29286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator