Theorem ralrimiva 2392

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 108	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2391	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311

This theorem is referenced by:  ralrimivvva  2402  rgen2  2405  rgen3  2406  nrexdv  2412  r19.29vva  2456  rabbidva  2548  ssrabdv  3019  ss2rabdv  3021  iuneq2dv  3678  disjeq2dv  3750  mpteq12dva  3838  triun  3867  issod  4056  frirrg  4087  frind  4089  peano2  4318  fun11iun  5147  fniinfv  5231  eqfnfv  5265  eqfnfvd  5268  dff3im  5312  dffo4  5315  foco2  5318  fmptd  5322  ffnfv  5323  fmpt2d  5327  ffvresb  5328  fconst2g  5376  fconstfvm  5379  resfunexg  5382  eufnfv  5389  fniunfv  5401  fcofo  5424  fliftel  5433  fliftfun  5436  fliftfuns  5438  riota5f  5492  grprinvlem  5695  grprinvd  5696  f1ocnvd  5702  suppssov1  5709  offval2  5726  ofrfval2  5727  offveqb  5730  caofref  5732  caofinvl  5733  opabex3d  5748  tfrlem1  5923  tfrlemisucaccv  5939  tfrlemiubacc  5944  omcl  6041  oeicl  6042  qliftfuns  6190  genprndl  6617  genprndu  6618  nqprloc  6641  ltexprlemrnd  6701  ltexprlemdisj  6702  lteupri  6713  recexprlemrnd  6725  recexprlemdisj  6726  caucvgprlemlim  6777  caucvgprprlemlim  6807  caucvgsrlembound  6876  caucvgsrlemgt1  6877  caucvgsrlemoffgt1  6881  caucvgsr  6884  elrealeu  6904  axcaucvglemcau  6970  axcaucvglemres  6971  negeu  7200  creur  7909  creui  7910  indstr2  8544  iooidg  8776  iccsupr  8833  icoshftf1o  8857  fznlem  8903  frecuzrdgfn  9172  iseqovex  9193  iseqval  9194  iseqfn  9195  iseq1  9196  iseqcl  9197  iseqf  9198  iseqp1  9199  iseqfveq2  9202  iseqfveq  9204  iseqfeq  9205  iseqshft2  9206  monoord  9209  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqcaopr2  9215  iseqid3s  9220  iseqid  9221  iseqhomo  9222  shftf  9405  caucvgrelemcau  9553  cvg1nlemcau  9557  cvg1nlemres  9558  resqrexlemcvg  9591  resqrexlemglsq  9594  resqrexlemga  9595  climconst  9785  2clim  9796  climcn1  9803  climcn2  9804  cn1lem  9808  climsqz  9829  climsqz2  9830  climcau  9840  climrecvg1n  9841  serif0  9845