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

Theorem keepel 3878
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 2503 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2503 . 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 3875 1  |-  if (
ph ,  A ,  B )  e.  C
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   ifcif 3812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3813
This theorem is referenced by:  ifex  3879  xaddf  11215  ccatfn  12293  sadcf  13670  ramcl  14111  setcepi  14977  abvtrivd  16947  mvridlemOLD  17514  mvrf1  17520  mplcoe3  17567  mplcoe3OLD  17568  psrbagsn  17599  evlslem1  17623  marep01ma  18488  dscmet  20187  dscopn  20188  i1f1lem  21189  i1f1  21190  itg2const  21240  cxpval  22131  cxpcl  22141  recxpcl  22142  sqff1o  22542  chtublem  22572  dchrmulid2  22613  bposlem1  22645  lgsval  22661  lgsfcl2  22663  lgscllem  22664  lgsval2lem  22667  lgsneg  22680  lgsdilem  22683  lgsdir2  22689  lgsdir  22691  lgsdi  22693  lgsne0  22694  dchrisum0flblem1  22779  dchrisum0flblem2  22780  dchrisum0fno1  22782  rpvmasum2  22783  omlsi  24829  sgnsf  26214  indfval  26495  ddemeas  26674  eulerpartlemb  26773  eulerpartlemgs2  26785  sqdivzi  27405  pw2f1ocnv  29412  flcidc  29557  arearect  29617
  Copyright terms: Public domain W3C validator