Theorem ralrimivw 2624

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
ralrimivw.1	|- ( ph -> ps )

Assertion

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

Distinct variable group:   ph, x

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

Proof of Theorem ralrimivw

Step	Hyp	Ref	Expression
1		ralrimivw.1	. . 3 |- ( ph -> ps )
2	1	a1d 22	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2622	1 |- ( ph -> A. x e. A ps )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  r19.27v  2678  r19.28v  2679  exse  4481  sosng  4848  dmxpm  5002  exse2  5161  funco  5417  acexmidlemph  6078  mpoeq12  6148  xpexgALT  6366  opabn1stprc  6429  mpoexg  6447  rdgtfr  6645  rdgruledefgg  6646  rdgivallem  6652  frecabex  6669  frectfr  6671  omfnex  6722  oeiv  6729  uniqs  6867  exmidpw2en  7219  exmidssfi  7246  sbthlemi5  7278  sbthlemi6  7279  updjud  7423  exmidfodomrlemim  7554  exmidaclem  7565  exmidapne  7627  cc4f  7636  genpdisj  7891  ltexprlemloc  7975  recexprlemloc  7999  cauappcvgprlemrnd  8018  cauappcvgprlemdisj  8019  caucvgprlemrnd  8041  caucvgprlemdisj  8042  caucvgprprlemrnd  8069  caucvgprprlemdisj  8070  suplocexpr  8093  zsupssdc  10684  nninfinf  10895  recan  11892  climconst  12075  sumeq2ad  12154  dvdsext  12641  pc11  13133  ptex  13671  imasex  13679  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfnlemg  13688  imasaddvallemg  13689  quslem  13698  grpinvfng  13902  prdsex  14256  prdsval  14257  prdsbaslemss  14258  prdsbas  14260  scaffng  14730  neif  15333  lmconst  15408  cndis  15433  plyval  15924  lgsquadlem2  16363  2sqlem10  16410  vtxdumgrfival  16705  uspgr2wlkeq2  16773  pw1dceq  17201  exmidnotnotr  17202  exmidcon  17203  exmidpeirce  17204  wexmiddiffi  17210  wexmiddifxy  17212