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  6619  genprndu  6620  nqprloc  6643  ltexprlemrnd  6703  ltexprlemdisj  6704  lteupri  6715  recexprlemrnd  6727  recexprlemdisj  6728  caucvgprlemlim  6779  caucvgprprlemlim  6809  caucvgsrlembound  6878  caucvgsrlemgt1  6879  caucvgsrlemoffgt1  6883  caucvgsr  6886  elrealeu  6906  axcaucvglemcau  6972  axcaucvglemres  6973  negeu  7202  creur  7911  creui  7912  indstr2  8546  iooidg  8778  iccsupr  8835  icoshftf1o  8859  fznlem  8905  frecuzrdgfn  9198  iseqovex  9219  iseqval  9220  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqf  9224  iseqp1  9225  iseqfveq2  9228  iseqfveq  9230  iseqfeq  9231  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqid3s  9246  iseqid  9247  iseqhomo  9248  shftf  9431  caucvgrelemcau  9579  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemcvg  9617  resqrexlemglsq  9620  resqrexlemga  9621  climconst  9811  2clim  9822  climcn1  9829  climcn2  9830  cn1lem  9834  climsqz  9855  climsqz2  9856  climcau  9866  climrecvg1n  9867  serif0  9871