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

Theorem r19.21bi 2801
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 2798 . . 3  |-  ( A. x  e.  A  ps  ->  ( x  e.  A  ->  ps ) )
31, 2syl 17 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
43imp 430 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787
This theorem is referenced by:  r19.21be  2803  rspec2  2804  rspec3  2805  ralxfr2d  4638  f1oresrab  6070  isoselem  6247  boxcutc  7573  xpf1o  7740  fineqvlem  7792  indexfi  7888  dffi3  7951  suppr  7993  supiso  7997  infpr  8019  ordtypelem9  8041  brwdom3  8097  xpwdomg  8100  ixpiunwdom  8106  infxpenc2lem1  8448  hsmexlem4  8857  gchina  9123  wunom  9144  prcdnq  9417  prnmax  9419  dedekind  9796  dedekindle  9797  monoord2  12241  seqshft  13127  limsupgre  13520  limsupgreOLD  13521  limsupbnd1  13522  limsupbnd1OLD  13523  limsupbnd2  13524  limsupbnd2OLD  13525  climmpt2  13615  rlimcld2  13620  rlimmptrcl  13649  lo1mptrcl  13663  o1mptrcl  13664  climsup  13711  sumpr  13787  sumtp  13788  fsum2dlem  13809  fsumiun  13859  fprod2dlem  14012  iserodd  14748  vdwlem1  14894  vdwlem6  14899  vdwnnlem3  14910  imasvscafn  15394  fuciso  15831  evlfcl  16058  yonedainv  16117  acsmapd  16375  prdsmndd  16520  psgnunilem5  17086  gsummpt1n0  17532  dprdspan  17595  ablfaclem2  17654  srgi  17680  srgrz  17694  srglz  17695  issrngd  18024  psrbaglesupp  18527  psrbagcon  18530  psrass1lem  18536  evlslem2  18670  mpfind  18694  gsumsmonply1  18832  gsummoncoe1  18833  evl1gsummon  18888  frgpcyg  19075  frlmgsum  19261  uvcresum  19282  cpmatmcllem  19673  neiptoptop  20078  neiptopnei  20079  ordtrest2lem  20150  cncmp  20338  1stckgenlem  20499  ptcld  20559  dfac14  20564  txcnp  20566  ptcnplem  20567  ptcnp  20568  ptcn  20573  pthaus  20584  xkococnlem  20605  xkococn  20606  cnmpt11  20609  cnmpt1t  20611  cnmpt12  20613  cnmptkp  20626  cnmptk1  20627  cnmptkk  20629  cnmptk1p  20631  cnmptk2  20632  cnmpt2k  20634  xpstopnlem1  20755  cnpflfi  20945  ptcmplem2  20999  cnextcn  21013  cnextfres1  21014  cnmpt1plusg  21033  cnmpt2plusg  21034  cnmpt1vsca  21139  cnmpt2vsca  21140  ustfilxp  21158  utoptop  21180  restutop  21183  restutopopn  21184  ucncn  21231  cfilufg  21239  trcfilu  21240  psmet0  21255  psmettri2  21256  prdsxmetlem  21314  prdsbl  21437  prdsxmslem2  21475  psmetutop  21513  cnmpt1ds  21771  cnmpt2ds  21772  cncfmpt2ss  21843  bndth  21882  cnmpt1ip  22111  cnmpt2ip  22112  iscmet3lem2  22155  cmetcusp1  22213  rrxcph  22244  ovoliunlem1  22333  ovoliunlem3  22335  ovoliun  22336  ovoliun2  22337  ovolscalem1  22344  volfiniun  22377  uniioombllem4  22421  mbfmptcl  22470  mbfeqalem  22475  mbfres2  22478  ismbf3d  22487  mbfsup  22497  mbfinf  22498  mbfinfOLD  22499  mbflim  22503  itg1ge0  22521  itg1mulc  22539  i1fposd  22542  itg1climres  22549  mbfi1fseqlem4  22553  itg2lea  22579  itg2splitlem  22583  itg2split  22584  itg2monolem1  22585  itg2mono  22588  itg2i1fseqle  22589  itg2i1fseq  22590  itg2addlem  22593  itg2cnlem1  22596  itgeqa  22648  itgss3  22649  itgfsum  22661  itgabs  22669  itggt0  22676  dvmptcl  22790  dvmptco  22803  dvlipcn  22823  dvle  22836  dvfsumle  22850  dvfsumge  22851  dvfsumabs  22852  dvmptrecl  22853  dvfsumlem2  22856  itgparts  22876  itgsubstlem  22877  itgsubst  22878  coeeulem  23046  dgrlem  23051  dgrlb  23058  coeaddlem  23071  coecj  23100  ulmss  23217  ulmdvlem2  23221  itgulm2  23229  logtayl  23470  leibpi  23733  xrlimcnp  23759  o1cxp  23765  jensen  23779  lgambdd  23827  wilthlem2  23859  sqff1o  23972  fsumdvdscom  23977  fsumdvdsmul  23987  dchrmulcl  24040  dchrmulid2  24043  dchrinv  24052  dchrisumlem3  24192  dchrvmasumlem2  24199  ostth1  24334  ercgrg  24424  f1otrg  24747  f1otrge  24748  ubthlem2  26358  fmptcof2  28099  disjdsct  28123  ressprs  28254  oduprs  28255  archiabl  28353  lmodslmd  28358  txomap  28500  qtophaus  28502  locfinreflem  28506  ordtrest2NEWlem  28567  lmdvg  28598  esumcl  28690  esumeq2d  28697  esumnul  28708  hasheuni  28745  esumcvg  28746  esumcvgre  28751  insiga  28798  ldsysgenld  28821  ldgenpisyslem1  28824  measvunilem  28873  measvunilem0  28874  measdivcstOLD  28885  cntmeas  28887  voliune  28891  volfiniune  28892  1stmbfm  28921  2ndmbfm  28922  omssubadd  28961  difelcarsg  28971  inelcarsg  28972  eulerpartlems  29019  eulerpartlemsv3  29020  eulerpartlemgvv  29035  dstrvprob  29130  bnj93  29462  bnj518  29485  bnj1489  29653  subfacp1lem3  29693  subfacp1lem5  29695  erdszelem8  29709  ptpcon  29744  rescon  29757  cvmliftmolem2  29793  cvmlift2lem11  29824  cvmliftphtlem  29828  mclsax  29995  fin2so  31635  poimirlem18  31661  poimirlem21  31664  mblfinlem2  31681  itgabsnc  31714  itggt0cn  31717  prdsbnd  31828  prdstotbnd  31829  prdsbnd2  31830  rrnequiv  31870  eqlkr3  32375  dih1dimatlem  34605  fnwe2lem1  35613  imo72b2  36255  rfcnnnub  36996  mptex2  37054  fompt  37089  suplesup  37170  climinf  37255  climinfOLD  37256  climsuse  37258  mullimc  37267  limccog  37271  mullimcf  37274  limcperiod  37279  limcleqr  37296  neglimc  37299  0ellimcdiv  37301  limclner  37303  dvdivbd  37366  ioodvbdlimc1lem1  37374  dvnprodlem2  37390  iblsplit  37411  stoweidlem5  37433  stoweidlem16  37444  stoweidlem21  37449  stoweidlem24  37452  stoweidlem25  37453  stoweidlem28  37456  stoweidlem31  37460  stoweidlem41  37470  stoweidlem42  37471  stoweidlem44  37473  stoweidlem45  37474  stoweidlem48  37477  stoweidlem51  37480  stoweidlem54  37483  stoweidlem57  37486  stoweidlem60  37489  stoweidlem62  37491  stoweidlem62OLD  37492  stirlinglem5  37508  dirkercncflem3  37535  fourierdlem11  37548  fourierdlem12  37549  fourierdlem14  37551  fourierdlem15  37552  fourierdlem31  37568  fourierdlem34  37571  fourierdlem41  37578  fourierdlem48  37585  fourierdlem49  37586  fourierdlem50  37587  fourierdlem54  37591  fourierdlem69  37606  fourierdlem73  37610  fourierdlem74  37611  fourierdlem75  37612  fourierdlem76  37613  fourierdlem79  37616  fourierdlem80  37617  fourierdlem81  37618  fourierdlem92  37629  fourierdlem93  37630  fourierdlem94  37631  fourierdlem97  37634  fourierdlem103  37640  fourierdlem104  37641  fourierdlem111  37648  fourierdlem113  37650  etransclem32  37697  caragendifcl  37843
  Copyright terms: Public domain W3C validator