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

Theorem elimel 3759
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 2472 . 2  |-  ( A  =  if ( A  e.  C ,  A ,  B )  ->  ( A  e.  C  <->  if ( A  e.  C ,  A ,  B )  e.  C ) )
2 eleq1 2472 . 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 3755 1  |-  if ( A  e.  C ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   ifcif 3707
This theorem is referenced by:  orduninsuc  4790  fprg  5882  oawordeu  6765  oeoa  6807  omopth  6868  unfilem3  7340  inar1  8614  supsr  8951  renegcl  9328  peano5uzti  10323  eluzadd  10478  eluzsub  10479  ltweuz  11264  uzenom  11267  seqfn  11298  seq1  11299  seqp1  11301  sqeqor  11458  binom2  11459  nn0opth2  11528  faclbnd4lem2  11548  hashxp  11660  dvdsle  12858  divalglem7  12882  divalg  12886  gcdaddm  12992  iblcnlem  19641  elimnv  22136  elimnvu  22137  nmlno0i  22256  nmblolbi  22262  blocn  22269  elimphu  22283  ubth  22336  htth  22382  hvsubsub4  22523  hvnegdi  22530  hvsubeq0  22531  hvaddcan  22533  hvsubadd  22540  normlem6  22578  normlem9at  22584  normsq  22597  normsub0  22599  norm-ii  22601  norm-iii  22603  normsub  22606  normpyth  22608  norm3dif  22613  norm3lemt  22615  norm3adifi  22616  normpar  22618  polid  22622  bcs  22644  hhssablo  22724  hhssnvt  22726  shscl  22781  shslej  22843  shincl  22844  pjhth  22856  omlsii  22866  ococ  22869  pjoc1  22897  pjoml  22899  pjoc2  22902  chm0  22954  chne0  22957  chocin  22958  chj0  22960  chincl  22962  chsscon3  22963  chlejb1  22975  chnle  22977  chjo  22978  chdmm1  22988  chjass  22996  ledi  23003  h1de2ci  23019  spansn  23022  elspansn  23029  elspansn2  23030  h1datom  23045  cmbr3  23071  pjoml2  23074  pjoml3  23075  cmcm  23077  cmcm3  23078  lecm  23080  osum  23108  spansnj  23110  spansncv  23116  pjch1  23133  pjadji  23148  pjaddi  23149  pjinormi  23150  pjsubi  23151  pjmuli  23152  pjige0  23154  pjcjt2  23155  pjch  23157  pjhfo  23169  pj11  23177  pjopyth  23183  pjnorm  23187  pjpyth  23188  pjnel  23189  eigre  23299  eigorth  23302  hoddi  23454  nmlnop0  23462  lnopeq0lem2  23470  lnopeq  23473  lnopunilem2  23475  lnopunii  23476  lnophmi  23482  nmbdoplb  23489  nmcopex  23493  nmcoplb  23494  lnopcon  23499  lnfn0  23511  lnfnmul  23512  nmcfnex  23517  nmcfnlb  23518  lnfncon  23520  riesz4  23528  riesz1  23529  cnlnadjeu  23542  pjhmop  23614  pjss2coi  23628  pjssmi  23629  pjssge0i  23630  pjdifnormi  23631  pjidmco  23645  mdslmd1lem3  23791  mdslmd1lem4  23792  csmdsymi  23798  cvmd  23800  hatomic  23824  chrelat2  23834  cvexch  23838  atord  23852  atcvat2  23853  mdsym  23876  kur14  24863  abs2sqle  25081  abs2sqlt  25082  ax5seglem8  25787  onsuccon  26100  onsucsuccmp  26106  sdclem1  26345  bnj941  28861  bnj944  29027
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-if 3708
  Copyright terms: Public domain W3C validator