Theorem ralrimiva 2434

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	|- ( ( ph /\ x e. A ) -> ps )

Assertion

Ref	Expression
ralrimiva	|- ( ph -> A. x e. A ps )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 |- ( ( ph /\ x e. A ) -> ps )
2	1	ex 113	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2433	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1433   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  ralrimivvva  2444  rgen2  2447  rgen3  2448  nrexdv  2454  r19.29vva  2500  rabbidva  2592  ssrabdv  3073  ss2rabdv  3075  iuneq2dv  3699  disjeq2dv  3771  mpteq12dva  3859  triun  3888  issod  4074  frirrg  4105  frind  4107  peano2  4336  fun11iun  5167  fniinfv  5252  eqfnfv  5286  eqfnfvd  5289  dff3im  5333  dffo4  5336  foco2  5339  fmptd  5343  ffnfv  5344  fmpt2d  5348  ffvresb  5349  fconst2g  5397  fconstfvm  5400  resfunexg  5403  eufnfv  5410  fniunfv  5422  fcofo  5444  fliftel  5453  fliftfun  5456  fliftfuns  5458  riota5f  5512  grprinvlem  5715  grprinvd  5716  f1ocnvd  5722  suppssov1  5729  offval2  5746  ofrfval2  5747  offveqb  5750  caofref  5752  caofinvl  5753  opabex3d  5768  f1od2  5876  tfrlem1  5946  tfrlemisucaccv  5962  tfrlemiubacc  5967  omcl  6064  oeicl  6065  qliftfuns  6213  eqsuptid  6410  eqinftid  6434  genprndl  6711  genprndu  6712  nqprloc  6735  ltexprlemrnd  6795  ltexprlemdisj  6796  lteupri  6807  recexprlemrnd  6819  recexprlemdisj  6820  caucvgprlemlim  6871  caucvgprprlemlim  6901  caucvgsrlembound  6970  caucvgsrlemgt1  6971  caucvgsrlemoffgt1  6975  caucvgsr  6978  elrealeu  6998  axcaucvglemcau  7064  axcaucvglemres  7065  negeu  7299  creur  8036  creui  8037  suprzclex  8445  supinfneg  8683  infsupneg  8684  indstr2  8696  iooidg  8932  iccsupr  8989  icoshftf1o  9013  fznlem  9060  exfzdc  9249  frecuzrdgfn  9414  iseqovex  9439  iseqval  9440  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqf  9444  iseqp1  9445  iseqfveq2  9448  iseqfveq  9450  iseqfeq  9451  iseqshft2  9452  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqid3s  9466  iseqid  9467  iseqhomo  9468  iseqz  9469  bccl  9694  shftf  9718  caucvgrelemcau  9866  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemcvg  9905  resqrexlemglsq  9908  resqrexlemga  9909  maxabslemval  10094  negfi  10110  minmax  10112  climconst  10129  2clim  10140  climcn1  10147  climcn2  10148  cn1lem  10152  climsqz  10173  climsqz2  10174  climcau  10184  climrecvg1n  10185  serif0  10189  dvdsssfz1  10252  zsupcllemstep  10341  infssuzex  10345  dvdsbnd  10348  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  dfgcd2  10403  coprmgcdb  10470  isprm6  10526