Theorem ralrimivw 2604

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  r19.27v  2658  r19.28v  2659  exse  4427  sosng  4792  dmxpm  4944  exse2  5102  funco  5358  acexmidlemph  6000  mpoeq12  6070  xpexgALT  6284  mpoexg  6363  rdgtfr  6526  rdgruledefgg  6527  rdgivallem  6533  frecabex  6550  frectfr  6552  omfnex  6603  oeiv  6610  uniqs  6748  exmidpw2en  7082  sbthlemi5  7136  sbthlemi6  7137  updjud  7257  exmidfodomrlemim  7387  exmidaclem  7398  exmidapne  7454  cc4f  7463  genpdisj  7718  ltexprlemloc  7802  recexprlemloc  7826  cauappcvgprlemrnd  7845  cauappcvgprlemdisj  7846  caucvgprlemrnd  7868  caucvgprlemdisj  7869  caucvgprprlemrnd  7896  caucvgprprlemdisj  7897  suplocexpr  7920  zsupssdc  10466  nninfinf  10673  recan  11628  climconst  11809  sumeq2ad  11888  dvdsext  12374  pc11  12862  ptex  13305  prdsex  13310  prdsval  13314  prdsbaslemss  13315  prdsbas  13317  imasex  13346  imasbas  13348  imasplusg  13349  imasmulr  13350  imasaddfnlemg  13355  imasaddvallemg  13356  quslem  13365  grpinvfng  13585  scaffng  14281  neif  14823  lmconst  14898  cndis  14923  plyval  15414  lgsquadlem2  15765  2sqlem10  15812  uspgr2wlkeq2  16087  pw1dceq  16396