Theorem r19.21bi 2932

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

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . 3 |- ( ph -> A. x e. A ps )
2		rsp 2929	. . 3 |- ( A. x e. A ps -> ( x e. A -> ps ) )
3	1, 2	syl 17	. 2 |- ( ph -> ( x e. A -> ps ) )
4	3	imp 445	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917

This theorem is referenced by:  r19.21be  2933  rspec2  2934  rspec3  2935  ralxfr2d  4882  mptex2  6384  f1oresrab  6395  isoselem  6591  boxcutc  7951  xpf1o  8122  fineqvlem  8174  indexfi  8274  dffi3  8337  suppr  8377  supiso  8381  infpr  8409  ordtypelem9  8431  brwdom3  8487  xpwdomg  8490  ixpiunwdom  8496  infxpenc2lem1  8842  hsmexlem4  9251  gchina  9521  wunom  9542  prcdnq  9815  prnmax  9817  dedekind  10200  dedekindle  10201  monoord2  12832  limsupgre  14212  limsupbnd1  14213  limsupbnd2  14214  climmpt2  14304  rlimcld2  14309  rlimmptrcl  14338  lo1mptrcl  14352  o1mptrcl  14353  climsup  14400  sumpr  14477  sumtp  14478  fsum2dlem  14501  fsumiun  14553  fprod2dlem  14710  iserodd  15540  vdwlem1  15685  vdwlem6  15690  vdwnnlem3  15701  imasvscafn  16197  fuciso  16635  evlfcl  16862  yonedainv  16921  acsmapd  17178  prdsmndd  17323  psgnunilem5  17914  gsummpt1n0  18364  dprdspan  18426  ablfaclem2  18485  srgi  18511  srgrz  18526  srglz  18527  issrngd  18861  psrbaglesupp  19368  psrbagcon  19371  psrass1lem  19377  evlslem2  19512  mpfind  19536  gsumsmonply1  19673  gsummoncoe1  19674  evl1gsummon  19729  frgpcyg  19922  frlmgsum  20111  uvcresum  20132  cpmatmcllem  20523  neiptoptop  20935  neiptopnei  20936  ordtrest2lem  21007  cncmp  21195  1stckgenlem  21356  ptcld  21416  dfac14  21421  txcnp  21423  ptcnplem  21424  ptcnp  21425  ptcn  21430  pthaus  21441  xkococnlem  21462  xkococn  21463  cnmpt11  21466  cnmpt1t  21468  cnmpt12  21470  cnmptkp  21483  cnmptk1  21484  cnmptkk  21486  cnmptk1p  21488  cnmptk2  21489  cnmpt2k  21491  xpstopnlem1  21612  cnpflfi  21803  ptcmplem2  21857  cnextcn  21871  cnextfres1  21872  cnmpt1plusg  21891  cnmpt2plusg  21892  cnmpt1vsca  21997  cnmpt2vsca  21998  ustfilxp  22016  utoptop  22038  restutop  22041  restutopopn  22042  ucncn  22089  cfilufg  22097  trcfilu  22098  psmet0  22113  psmettri2  22114  prdsxmetlem  22173  prdsbl  22296  prdsxmslem2  22334  psmetutop  22372  cnmpt1ds  22645  cnmpt2ds  22646  cncfmpt2ss  22718  bndth  22757  cnmpt1ip  23046  cnmpt2ip  23047  iscmet3lem2  23090  cmetcusp1  23149  rrxcph  23180  ovoliunlem1  23270  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  ovolscalem1  23281  volfiniun  23315  uniioombllem4  23354  mbfmptcl  23404  mbfeqalem  23409  mbfres2  23412  ismbf3d  23421  mbfsup  23431  mbfinf  23432  mbflim  23435  itg1ge0  23453  itg1mulc  23471  i1fposd  23474  itg1climres  23481  mbfi1fseqlem4  23485  itg2lea  23511  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq  23522  itg2addlem  23525  itg2cnlem1  23528  itgeqa  23580  itgss3  23581  itgfsum  23593  itgabs  23601  itggt0  23608  dvmptcl  23722  dvmptco  23735  dvlipcn  23757  dvle  23770  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvmptrecl  23787  dvfsumlem2  23790  itgparts  23810  itgsubstlem  23811  itgsubst  23812  coeeulem  23980  dgrlem  23985  dgrlb  23992  coeaddlem  24005  coecj  24034  ulmss  24151  ulmdvlem2  24155  itgulm2  24163  logtayl  24406  leibpi  24669  xrlimcnp  24695  o1cxp  24701  jensen  24715  lgambdd  24763  wilthlem2  24795  sqff1o  24908  fsumdvdscom  24911  fsumdvdsmul  24921  dchrmulcl  24974  dchrmulid2  24977  dchrinv  24986  dchrisumlem3  25180  dchrvmasumlem2  25187  ostth1  25322  ercgrg  25412  f1otrg  25751  f1otrge  25752  ubthlem2  27727  fmptcof2  29457  disjdsct  29480  fprodex01  29571  ressprs  29655  oduprs  29656  archiabl  29752  lmodslmd  29757  txomap  29901  qtophaus  29903  locfinreflem  29907  ordtrest2NEWlem  29968  lmdvg  29999  prodindf  30085  esumcl  30092  esumeq2d  30099  esumnul  30110  hasheuni  30147  esumcvg  30148  esumcvgre  30153  insiga  30200  ldsysgenld  30223  ldgenpisyslem1  30226  measvunilem  30275  measvunilem0  30276  measdivcstOLD  30287  cntmeas  30289  voliune  30292  volfiniune  30293  1stmbfm  30322  2ndmbfm  30323  omssubadd  30362  difelcarsg  30372  inelcarsg  30373  eulerpartlems  30422  eulerpartlemsv3  30423  eulerpartlemgvv  30438  dstrvprob  30533  hashreprin  30698  reprgt  30699  breprexplemc  30710  circlemeth  30718  hgt750lema  30735  tgoldbachgtd  30740  bnj93  30933  bnj518  30956  bnj1489  31124  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem8  31180  ptpconn  31215  resconn  31228  cvmliftmolem2  31264  cvmlift2lem11  31295  cvmliftphtlem  31299  mclsax  31466  conway  31910  slerec  31923  fin2so  33396  poimirlem18  33427  poimirlem21  33430  mblfinlem2  33447  itgabsnc  33479  itggt0cn  33482  prdsbnd  33592  prdstotbnd  33593  prdsbnd2  33594  rrnequiv  33634  eqlkr3  34388  dih1dimatlem  36618  fnwe2lem1  37620  imo72b2  38475  rfcnnnub  39195  disjxp1  39238  fompt  39379  fvixp2  39389  dmrelrnrel  39419  fvmptelrn  39428  suplesup  39555  infxr  39583  climinf  39838  climsuse  39840  mullimc  39848  limccog  39852  mullimcf  39855  limcperiod  39860  limcleqr  39876  neglimc  39879  0ellimcdiv  39881  limclner  39883  limsuppnfdlem  39933  limsupubuzlem  39944  xlimmnfvlem2  40059  xlimpnfvlem2  40063  climxlim2lem  40071  dvdivbd  40138  ioodvbdlimc1lem1  40146  dvnprodlem2  40162  iblsplit  40182  stoweidlem5  40222  stoweidlem16  40233  stoweidlem21  40238  stoweidlem24  40241  stoweidlem25  40242  stoweidlem28  40245  stoweidlem31  40248  stoweidlem41  40258  stoweidlem42  40259  stoweidlem44  40261  stoweidlem45  40262  stoweidlem48  40265  stoweidlem51  40268  stoweidlem54  40271  stoweidlem57  40274  stoweidlem60  40277  stoweidlem62  40279  stirlinglem5  40295  dirkercncflem3  40322  fourierdlem11  40335  fourierdlem12  40336  fourierdlem14  40338  fourierdlem15  40339  fourierdlem31  40355  fourierdlem34  40358  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem54  40377  fourierdlem69  40392  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem79  40402  fourierdlem80  40403  fourierdlem81  40404  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem113  40436  etransclem32  40483  subsaliuncllem  40575  sge0rpcpnf  40638  caragendifcl  40728  iinhoiicclem  40887  pimdecfgtioc  40925  issmfgtlem  40964