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

Theorem keepel 3740
Description: Keep a membership hypothesis for weak deduction theorem, when special case  B  e.  C is provable. (Contributed by NM, 14-Aug-1999.)
Hypotheses
Ref Expression
keepel.1  |-  A  e.  C
keepel.2  |-  B  e.  C
Assertion
Ref Expression
keepel  |-  if (
ph ,  A ,  B )  e.  C

Proof of Theorem keepel
StepHypRef Expression
1 eleq1 2448 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2448 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
3 keepel.1 . 2  |-  A  e.  C
4 keepel.2 . 2  |-  B  e.  C
51, 2, 3, 4keephyp 3737 1  |-  if (
ph ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   ifcif 3683
This theorem is referenced by:  ifex  3741  xaddf  10743  ccatfn  11669  sadcf  12893  ramcl  13325  setcepi  14171  abvtrivd  15856  mvridlem  16411  mvrf1  16417  mplcoe3  16457  psrbagsn  16483  dscmet  18492  dscopn  18493  i1f1lem  19449  i1f1  19450  itg2const  19500  evlslem1  19804  cxpval  20423  cxpcl  20433  recxpcl  20434  sqff1o  20833  chtublem  20863  dchrmulid2  20904  bposlem1  20936  lgsval  20952  lgsfcl2  20954  lgscllem  20955  lgsval2lem  20958  lgsneg  20971  lgsdilem  20974  lgsdir2  20980  lgsdir  20982  lgsdi  20984  lgsne0  20985  dchrisum0flblem1  21070  dchrisum0flblem2  21071  dchrisum0fno1  21073  rpvmasum2  21074  omlsi  22755  indfval  24211  sqdivzi  24964  pw2f1ocnv  26800  flcidc  27049
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
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 2375  df-cleq 2381  df-clel 2384  df-if 3684
  Copyright terms: Public domain W3C validator