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

Theorem keepel 3622
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 2343 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2343 . 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 3619 1  |-  if (
ph ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   ifcif 3565
This theorem is referenced by:  ifex  3623  xaddf  10551  ccatfn  11427  sadcf  12644  ramcl  13076  setcepi  13920  abvtrivd  15605  mvridlem  16164  mvrf1  16170  mplcoe3  16210  psrbagsn  16236  dscmet  18095  dscopn  18096  i1f1lem  19044  i1f1  19045  itg2const  19095  evlslem1  19399  cxpval  20011  cxpcl  20021  recxpcl  20022  sqff1o  20420  chtublem  20450  dchrmulid2  20491  bposlem1  20523  lgsval  20539  lgsfcl2  20541  lgscllem  20542  lgsval2lem  20545  lgsneg  20558  lgsdilem  20561  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsne0  20572  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0fno1  20660  rpvmasum2  20661  omlsi  21983  indfval  23600  sqdivzi  24079  pw2f1ocnv  27130  flcidc  27379
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