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

Theorem keepel 3996
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 2526 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2526 . 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 3993 1  |-  if (
ph ,  A ,  B )  e.  C
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   ifcif 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930
This theorem is referenced by:  ifex  3997  xaddf  11426  ccatfnOLD  12580  sadcf  14187  ramcl  14631  setcepi  15566  abvtrivd  17684  mvridlemOLD  18270  mvrf1  18276  mplcoe3  18323  mplcoe3OLD  18324  psrbagsn  18355  evlslem1  18379  marep01ma  19329  dscmet  21259  dscopn  21260  i1f1lem  22262  i1f1  22263  itg2const  22313  cxpval  23213  cxpcl  23223  recxpcl  23224  sqff1o  23654  chtublem  23684  dchrmulid2  23725  bposlem1  23757  lgsval  23773  lgsfcl2  23775  lgscllem  23776  lgsval2lem  23779  lgsneg  23792  lgsdilem  23795  lgsdir2  23801  lgsdir  23803  lgsdi  23805  lgsne0  23806  dchrisum0flblem1  23891  dchrisum0flblem2  23892  dchrisum0fno1  23894  rpvmasum2  23895  omlsi  26520  sgnsf  27953  indfval  28246  ddemeas  28445  eulerpartlemb  28571  eulerpartlemgs2  28583  sqdivzi  29345  pw2f1ocnv  31218  flcidc  31364  arearect  31424  sqwvfourb  32251  fouriersw  32253
  Copyright terms: Public domain W3C validator