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

Theorem keepel 3788
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 2495 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2495 . 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 3785 1  |-  if (
ph ,  A ,  B )  e.  C
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   ifcif 3731
This theorem is referenced by:  ifex  3789  xaddf  10802  ccatfn  11733  sadcf  12957  ramcl  13389  setcepi  14235  abvtrivd  15920  mvridlem  16475  mvrf1  16481  mplcoe3  16521  psrbagsn  16547  dscmet  18612  dscopn  18613  i1f1lem  19573  i1f1  19574  itg2const  19624  evlslem1  19928  cxpval  20547  cxpcl  20557  recxpcl  20558  sqff1o  20957  chtublem  20987  dchrmulid2  21028  bposlem1  21060  lgsval  21076  lgsfcl2  21078  lgscllem  21079  lgsval2lem  21082  lgsneg  21095  lgsdilem  21098  lgsdir2  21104  lgsdir  21106  lgsdi  21108  lgsne0  21109  dchrisum0flblem1  21194  dchrisum0flblem2  21195  dchrisum0fno1  21197  rpvmasum2  21198  omlsi  22898  indfval  24406  sqdivzi  25176  pw2f1ocnv  27099  flcidc  27347
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator