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

Theorem elimel 3815
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 2502 . 2  |-  ( A  =  if ( A  e.  C ,  A ,  B )  ->  ( A  e.  C  <->  if ( A  e.  C ,  A ,  B )  e.  C ) )
2 eleq1 2502 . 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 3811 1  |-  if ( A  e.  C ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1727   ifcif 3763
This theorem is referenced by:  orduninsuc  4852  fprg  5944  oawordeu  6827  oeoa  6869  omopth  6930  unfilem3  7402  inar1  8681  supsr  9018  renegcl  9395  peano5uzti  10390  eluzadd  10545  eluzsub  10546  ltweuz  11332  uzenom  11335  seqfn  11366  seq1  11367  seqp1  11369  sqeqor  11526  binom2  11527  nn0opth2  11596  faclbnd4lem2  11616  hashxp  11728  dvdsle  12926  divalglem7  12950  divalg  12954  gcdaddm  13060  iblcnlem  19709  elimnv  22206  elimnvu  22207  nmlno0i  22326  nmblolbi  22332  blocn  22339  elimphu  22353  ubth  22406  htth  22452  hvsubsub4  22593  hvnegdi  22600  hvsubeq0  22601  hvaddcan  22603  hvsubadd  22610  normlem6  22648  normlem9at  22654  normsq  22667  normsub0  22669  norm-ii  22671  norm-iii  22673  normsub  22676  normpyth  22678  norm3dif  22683  norm3lemt  22685  norm3adifi  22686  normpar  22688  polid  22692  bcs  22714  hhssablo  22794  hhssnvt  22796  shscl  22851  shslej  22913  shincl  22914  pjhth  22926  omlsii  22936  ococ  22939  pjoc1  22967  pjoml  22969  pjoc2  22972  chm0  23024  chne0  23027  chocin  23028  chj0  23030  chincl  23032  chsscon3  23033  chlejb1  23045  chnle  23047  chjo  23048  chdmm1  23058  chjass  23066  ledi  23073  h1de2ci  23089  spansn  23092  elspansn  23099  elspansn2  23100  h1datom  23115  cmbr3  23141  pjoml2  23144  pjoml3  23145  cmcm  23147  cmcm3  23148  lecm  23150  osum  23178  spansnj  23180  spansncv  23186  pjch1  23203  pjadji  23218  pjaddi  23219  pjinormi  23220  pjsubi  23221  pjmuli  23222  pjige0  23224  pjcjt2  23225  pjch  23227  pjhfo  23239  pj11  23247  pjopyth  23253  pjnorm  23257  pjpyth  23258  pjnel  23259  eigre  23369  eigorth  23372  hoddi  23524  nmlnop0  23532  lnopeq0lem2  23540  lnopeq  23543  lnopunilem2  23545  lnopunii  23546  lnophmi  23552  nmbdoplb  23559  nmcopex  23563  nmcoplb  23564  lnopcon  23569  lnfn0  23581  lnfnmul  23582  nmcfnex  23587  nmcfnlb  23588  lnfncon  23590  riesz4  23598  riesz1  23599  cnlnadjeu  23612  pjhmop  23684  pjss2coi  23698  pjssmi  23699  pjssge0i  23700  pjdifnormi  23701  pjidmco  23715  mdslmd1lem3  23861  mdslmd1lem4  23862  csmdsymi  23868  cvmd  23870  hatomic  23894  chrelat2  23904  cvexch  23908  atord  23922  atcvat2  23923  mdsym  23946  kur14  24933  abs2sqle  25151  abs2sqlt  25152  ax5seglem8  25906  onsuccon  26219  onsucsuccmp  26225  sdclem1  26485  bnj941  29241  bnj944  29407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3764
  Copyright terms: Public domain W3C validator