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

Theorem elimel 3617
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 2343 . 2  |-  ( A  =  if ( A  e.  C ,  A ,  B )  ->  ( A  e.  C  <->  if ( A  e.  C ,  A ,  B )  e.  C ) )
2 eleq1 2343 . 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 3613 1  |-  if ( A  e.  C ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   ifcif 3565
This theorem is referenced by:  orduninsuc  4634  oawordeu  6553  oeoa  6595  omopth  6656  unfilem3  7123  inar1  8397  supsr  8734  renegcl  9110  peano5uzti  10101  eluzadd  10256  eluzsub  10257  ltweuz  11024  uzenom  11027  seqfn  11058  seq1  11059  seqp1  11061  sqeqor  11217  binom2  11218  nn0opth2  11287  faclbnd4lem2  11307  hashxp  11386  dvdsle  12574  divalglem7  12598  divalg  12602  gcdaddm  12708  iblcnlem  19143  elimnv  21252  elimnvu  21253  nmlno0i  21372  nmblolbi  21378  blocn  21385  elimphu  21399  ubth  21452  htth  21498  hvsubsub4  21639  hvnegdi  21646  hvsubeq0  21647  hvaddcan  21649  hvsubadd  21656  normlem6  21694  normlem9at  21700  normsq  21713  normsub0  21715  norm-ii  21717  norm-iii  21719  normsub  21722  normpyth  21724  norm3dif  21729  norm3lemt  21731  norm3adifi  21732  normpar  21734  polid  21738  bcs  21760  hhssablo  21840  hhssnvt  21842  shscl  21897  shslej  21959  shincl  21960  pjhth  21972  omlsii  21982  ococ  21985  pjoc1  22013  pjoml  22015  pjoc2  22018  chm0  22070  chne0  22073  chocin  22074  chj0  22076  chincl  22078  chsscon3  22079  chlejb1  22091  chnle  22093  chjo  22094  chdmm1  22104  chjass  22112  ledi  22119  h1de2ci  22135  spansn  22138  elspansn  22145  elspansn2  22146  h1datom  22161  cmbr3  22187  pjoml2  22190  pjoml3  22191  cmcm  22193  cmcm3  22194  lecm  22196  osum  22224  spansnj  22226  spansncv  22232  pjch1  22249  pjadji  22264  pjaddi  22265  pjinormi  22266  pjsubi  22267  pjmuli  22268  pjige0  22270  pjcjt2  22271  pjch  22273  pjhfo  22285  pj11  22293  pjopyth  22299  pjnorm  22303  pjpyth  22304  pjnel  22305  eigre  22415  eigorth  22418  hoddi  22570  nmlnop0  22578  lnopeq0lem2  22586  lnopeq  22589  lnopunilem2  22591  lnopunii  22592  lnophmi  22598  nmbdoplb  22605  nmcopex  22609  nmcoplb  22610  lnopcon  22615  lnfn0  22627  lnfnmul  22628  nmcfnex  22633  nmcfnlb  22634  lnfncon  22636  riesz4  22644  riesz1  22645  cnlnadjeu  22658  pjhmop  22730  pjss2coi  22744  pjssmi  22745  pjssge0i  22746  pjdifnormi  22747  pjidmco  22761  mdslmd1lem3  22907  mdslmd1lem4  22908  csmdsymi  22914  cvmd  22916  hatomic  22940  chrelat2  22950  cvexch  22954  atord  22968  atcvat2  22969  mdsym  22992  kur14  23747  abs2sqle  24016  abs2sqlt  24017  ax5seglem8  24564  onsuccon  24877  onsucsuccmp  24883  alexeqd  24962  ac5g  25075  snelpwg  25091  ab2rexexg  25122  fprg  25133  hmeogrp  25537  cnegvex2b  25662  rnegvex2b  25663  ishomd  25790  selsubf3g  25992  sdclem1  26453  bnj941  28804  bnj944  28970
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator