Theorem ralrimivw 2571

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 2569	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  r19.27v  2624  r19.28v  2625  exse  4372  sosng  4737  dmxpm  4887  exse2  5044  funco  5299  acexmidlemph  5918  mpoeq12  5986  xpexgALT  6199  mpoexg  6278  rdgtfr  6441  rdgruledefgg  6442  rdgivallem  6448  frecabex  6465  frectfr  6467  omfnex  6516  oeiv  6523  uniqs  6661  exmidpw2en  6982  sbthlemi5  7036  sbthlemi6  7037  updjud  7157  exmidfodomrlemim  7282  exmidaclem  7293  exmidapne  7345  cc4f  7354  genpdisj  7609  ltexprlemloc  7693  recexprlemloc  7717  cauappcvgprlemrnd  7736  cauappcvgprlemdisj  7737  caucvgprlemrnd  7759  caucvgprlemdisj  7760  caucvgprprlemrnd  7787  caucvgprprlemdisj  7788  suplocexpr  7811  zsupssdc  10347  nninfinf  10554  recan  11293  climconst  11474  sumeq2ad  11553  dvdsext  12039  pc11  12527  ptex  12968  prdsex  12973  prdsval  12977  prdsbaslemss  12978  prdsbas  12980  imasex  13009  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfnlemg  13018  imasaddvallemg  13019  quslem  13028  grpinvfng  13248  scaffng  13943  neif  14485  lmconst  14560  cndis  14585  plyval  15076  lgsquadlem2  15427  2sqlem10  15474