Theorem ralrimivw 2606

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

Hypothesis

Ref	Expression
ralrimivw.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralrimivw	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimivw

Step	Hyp	Ref	Expression
1		ralrimivw.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 2604	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2202  ∀wral 2510

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  r19.27v  2660  r19.28v  2661  exse  4433  sosng  4799  dmxpm  4952  exse2  5110  funco  5366  acexmidlemph  6011  mpoeq12  6081  xpexgALT  6295  opabn1stprc  6358  mpoexg  6376  rdgtfr  6540  rdgruledefgg  6541  rdgivallem  6547  frecabex  6564  frectfr  6566  omfnex  6617  oeiv  6624  uniqs  6762  exmidpw2en  7104  exmidssfi  7131  sbthlemi5  7160  sbthlemi6  7161  updjud  7281  exmidfodomrlemim  7412  exmidaclem  7423  exmidapne  7479  cc4f  7488  genpdisj  7743  ltexprlemloc  7827  recexprlemloc  7851  cauappcvgprlemrnd  7870  cauappcvgprlemdisj  7871  caucvgprlemrnd  7893  caucvgprlemdisj  7894  caucvgprprlemrnd  7921  caucvgprprlemdisj  7922  suplocexpr  7945  zsupssdc  10499  nninfinf  10706  recan  11687  climconst  11868  sumeq2ad  11947  dvdsext  12434  pc11  12922  ptex  13365  prdsex  13370  prdsval  13374  prdsbaslemss  13375  prdsbas  13377  imasex  13406  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfnlemg  13415  imasaddvallemg  13416  quslem  13425  grpinvfng  13645  scaffng  14342  neif  14884  lmconst  14959  cndis  14984  plyval  15475  lgsquadlem2  15826  2sqlem10  15873  vtxdumgrfival  16168  uspgr2wlkeq2  16236  pw1dceq  16656