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

Theorem keepel 4013
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 2539 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2539 . 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 4010 1  |-  if (
ph ,  A ,  B )  e.  C
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   ifcif 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3946
This theorem is referenced by:  ifex  4014  xaddf  11435  ccatfn  12571  sadcf  13979  ramcl  14423  setcepi  15290  abvtrivd  17360  mvridlemOLD  17945  mvrf1  17951  mplcoe3  17998  mplcoe3OLD  17999  psrbagsn  18030  evlslem1  18054  marep01ma  19031  dscmet  20961  dscopn  20962  i1f1lem  21964  i1f1  21965  itg2const  22015  cxpval  22911  cxpcl  22921  recxpcl  22922  sqff1o  23322  chtublem  23352  dchrmulid2  23393  bposlem1  23425  lgsval  23441  lgsfcl2  23443  lgscllem  23444  lgsval2lem  23447  lgsneg  23460  lgsdilem  23463  lgsdir2  23469  lgsdir  23471  lgsdi  23473  lgsne0  23474  dchrisum0flblem1  23559  dchrisum0flblem2  23560  dchrisum0fno1  23562  rpvmasum2  23563  omlsi  26145  sgnsf  27543  indfval  27855  ddemeas  28033  eulerpartlemb  28132  eulerpartlemgs2  28144  sqdivzi  28929  pw2f1ocnv  30907  flcidc  31052  arearect  31112  sqwvfourb  31853  fourierswlem  31854  fouriersw  31855
  Copyright terms: Public domain W3C validator