Theorem ralrimivw 2618

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 2616	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2205   A.wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  r19.27v  2672  r19.28v  2673  exse  4462  sosng  4828  dmxpm  4982  exse2  5141  funco  5397  acexmidlemph  6051  mpoeq12  6121  xpexgALT  6339  opabn1stprc  6402  mpoexg  6420  rdgtfr  6618  rdgruledefgg  6619  rdgivallem  6625  frecabex  6642  frectfr  6644  omfnex  6695  oeiv  6702  uniqs  6840  exmidpw2en  7185  exmidssfi  7212  sbthlemi5  7244  sbthlemi6  7245  updjud  7386  exmidfodomrlemim  7517  exmidaclem  7528  exmidapne  7590  cc4f  7599  genpdisj  7854  ltexprlemloc  7938  recexprlemloc  7962  cauappcvgprlemrnd  7981  cauappcvgprlemdisj  7982  caucvgprlemrnd  8004  caucvgprlemdisj  8005  caucvgprprlemrnd  8032  caucvgprprlemdisj  8033  suplocexpr  8056  zsupssdc  10622  nninfinf  10829  recan  11819  climconst  12000  sumeq2ad  12079  dvdsext  12566  pc11  13054  ptex  13561  imasex  13569  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfnlemg  13578  imasaddvallemg  13579  quslem  13588  grpinvfng  13799  prdsex  14114  prdsval  14115  prdsbaslemss  14116  prdsbas  14118  scaffng  14583  neif  15132  lmconst  15207  cndis  15232  plyval  15723  lgsquadlem2  16077  2sqlem10  16124  vtxdumgrfival  16419  uspgr2wlkeq2  16487  pw1dceq  16904  exmidnotnotr  16905  exmidcon  16906  exmidpeirce  16907