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

Theorem r19.21bi 2751
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.)
Hypothesis
Ref Expression
r19.21bi.1  |-  ( ph  ->  A. x  e.  A  ps )
Assertion
Ref Expression
r19.21bi  |-  ( (
ph  /\  x  e.  A )  ->  ps )

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . 3  |-  ( ph  ->  A. x  e.  A  ps )
2 rsp 2748 . . 3  |-  ( A. x  e.  A  ps  ->  ( x  e.  A  ->  ps ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
43imp 427 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1826   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-12 1862
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-ral 2737
This theorem is referenced by:  r19.21be  2753  rspec2  2754  rspec3  2755  ralxfr2d  4578  f1oresrab  5965  isoselem  6138  boxcutc  7431  xpf1o  7598  fineqvlem  7650  indexfi  7743  dffi3  7806  suppr  7844  supiso  7848  ordtypelem9  7866  brwdom3  7923  xpwdomg  7926  ixpiunwdom  7932  infxpenc2lem1  8309  hsmexlem4  8722  gchina  8988  wunom  9009  prcdnq  9282  prnmax  9284  dedekind  9655  dedekindle  9656  monoord2  12041  seqshft  12920  limsupgre  13306  limsupbnd1  13307  limsupbnd2  13308  climmpt2  13398  rlimcld2  13403  rlimmptrcl  13432  lo1mptrcl  13446  o1mptrcl  13447  climsup  13494  fsum2dlem  13587  fsumiun  13637  fprod2dlem  13786  iserodd  14361  vdwlem1  14501  vdwlem6  14506  vdwnnlem3  14517  imasvscafn  14944  fuciso  15381  evlfcl  15608  yonedainv  15667  acsmapd  15925  prdsmndd  16070  psgnunilem5  16636  gsummpt1n0  17106  dprdspan  17187  ablfaclem2  17250  srgi  17276  srgrz  17290  srglz  17291  issrngd  17623  psrbaglesupp  18130  psrbaglesuppOLD  18131  psrbagcon  18135  psrass1lem  18142  evlslem2  18293  mpfind  18318  gsumsmonply1  18458  gsummoncoe1  18459  evl1gsummon  18514  frgpcyg  18703  frlmgsumOLD  18890  frlmgsum  18891  uvcresum  18913  cpmatmcllem  19304  neiptoptop  19718  neiptopnei  19719  ordtrest2lem  19790  cncmp  19978  1stckgenlem  20139  ptcld  20199  dfac14  20204  txcnp  20206  ptcnplem  20207  ptcnp  20208  ptcn  20213  pthaus  20224  xkococnlem  20245  xkococn  20246  cnmpt11  20249  cnmpt1t  20251  cnmpt12  20253  cnmptkp  20266  cnmptk1  20267  cnmptkk  20269  cnmptk1p  20271  cnmptk2  20272  cnmpt2k  20274  xpstopnlem1  20395  cnpflfi  20585  ptcmplem2  20638  cnextcn  20652  cnextfres  20653  cnmpt1plusg  20671  cnmpt2plusg  20672  cnmpt1vsca  20781  cnmpt2vsca  20782  ustfilxp  20800  utoptop  20822  restutop  20825  restutopopn  20826  ucncn  20873  cfilufg  20881  trcfilu  20882  psmet0  20897  psmettri2  20898  prdsxmetlem  20956  prdsbl  21079  prdsxmslem2  21117  metutopOLD  21170  psmetutop  21171  cnmpt1ds  21432  cnmpt2ds  21433  cncfmpt2ss  21504  bndth  21543  cnmpt1ip  21772  cnmpt2ip  21773  iscmet3lem2  21816  cmetcusp1OLD  21876  cmetcusp1  21877  rrxcph  21909  ovoliunlem1  21998  ovoliunlem3  22000  ovoliun  22001  ovoliun2  22002  ovolscalem1  22009  volfiniun  22042  uniioombllem4  22080  mbfmptcl  22129  mbfeqalem  22134  mbfres2  22137  ismbf3d  22146  mbfsup  22156  mbfinf  22157  mbflim  22160  itg1ge0  22178  itg1mulc  22196  i1fposd  22199  itg1climres  22206  mbfi1fseqlem4  22210  itg2lea  22236  itg2splitlem  22240  itg2split  22241  itg2monolem1  22242  itg2mono  22245  itg2i1fseqle  22246  itg2i1fseq  22247  itg2addlem  22250  itg2cnlem1  22253  itgeqa  22305  itgss3  22306  itgfsum  22318  itgabs  22326  itggt0  22333  dvmptcl  22447  dvmptco  22460  dvlipcn  22480  dvle  22493  dvfsumle  22507  dvfsumge  22508  dvfsumabs  22509  dvmptrecl  22510  dvfsumlem2  22513  itgparts  22533  itgsubstlem  22534  itgsubst  22535  coeeulem  22706  dgrlem  22711  dgrlb  22718  coeaddlem  22731  coecj  22760  ulmss  22877  ulmdvlem2  22881  itgulm2  22889  logtayl  23128  leibpi  23389  xrlimcnp  23415  o1cxp  23421  jensen  23435  wilthlem2  23460  sqff1o  23573  fsumdvdscom  23578  fsumdvdsmul  23588  dchrmulcl  23641  dchrmulid2  23644  dchrinv  23653  dchrisumlem3  23793  dchrvmasumlem2  23800  ostth1  23935  ercgrg  24028  f1otrg  24295  f1otrge  24296  ubthlem2  25904  fmptcof2  27643  disjdsct  27668  ressprs  27796  oduprs  27797  archiabl  27895  lmodslmd  27900  sumpr  27922  txomap  27991  qtophaus  27993  locfinreflem  27997  ordtrest2NEWlem  28058  lmdvg  28089  esumcl  28178  esumeq2d  28185  esumnul  28196  hasheuni  28233  esumcvg  28234  esumcvgre  28239  insiga  28286  measvunilem  28339  measvunilem0  28340  measdivcstOLD  28351  cntmeas  28353  voliune  28357  volfiniune  28358  1stmbfm  28387  2ndmbfm  28388  omssubadd  28427  difelcarsg  28437  inelcarsg  28438  eulerpartlems  28482  eulerpartlemsv3  28483  eulerpartlemgvv  28498  dstrvprob  28593  lgambdd  28768  subfacp1lem3  28815  subfacp1lem5  28817  erdszelem8  28831  ptpcon  28867  rescon  28880  cvmliftmolem2  28916  cvmlift2lem11  28947  cvmliftphtlem  28951  mclsax  29118  fin2so  30205  mblfinlem2  30217  itgabsnc  30250  itggt0cn  30253  prdsbnd  30455  prdstotbnd  30456  prdsbnd2  30457  rrnequiv  30497  fnwe2lem1  31162  rfcnnnub  31578  mptex2  31612  climinf  31778  climsuse  31780  mullimc  31788  limccog  31792  mullimcf  31795  limcperiod  31800  limcleqr  31816  neglimc  31819  0ellimcdiv  31821  limclner  31823  dvdivbd  31886  ioodvbdlimc1lem1  31894  dvnprodlem2  31910  iblsplit  31931  stoweidlem5  31953  stoweidlem16  31964  stoweidlem21  31969  stoweidlem24  31972  stoweidlem25  31973  stoweidlem28  31976  stoweidlem31  31979  stoweidlem41  31989  stoweidlem42  31990  stoweidlem44  31992  stoweidlem45  31993  stoweidlem48  31996  stoweidlem51  31999  stoweidlem54  32002  stoweidlem57  32005  stoweidlem60  32008  stoweidlem62  32010  stirlinglem5  32026  dirkercncflem3  32053  fourierdlem11  32066  fourierdlem12  32067  fourierdlem14  32069  fourierdlem15  32070  fourierdlem31  32086  fourierdlem34  32089  fourierdlem41  32096  fourierdlem48  32103  fourierdlem49  32104  fourierdlem50  32105  fourierdlem54  32109  fourierdlem69  32124  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem79  32134  fourierdlem80  32135  fourierdlem81  32136  fourierdlem92  32147  fourierdlem93  32148  fourierdlem94  32149  fourierdlem97  32152  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem113  32168  etransclem32  32215  bnj93  34268  bnj518  34291  bnj1489  34459  eqlkr3  35239  dih1dimatlem  37469  imo72b2  38522
  Copyright terms: Public domain W3C validator