Theorem ralrimivw 2540

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

Syntax hints:   → wi 4   ∈ wcel 2136  ∀wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  r19.27v  2593  r19.28v  2594  exse  4314  sosng  4677  dmxpm  4824  exse2  4978  funco  5228  acexmidlemph  5835  mpoeq12  5902  xpexgALT  6101  mpoexg  6179  rdgtfr  6342  rdgruledefgg  6343  rdgivallem  6349  frecabex  6366  frectfr  6368  omfnex  6417  oeiv  6424  uniqs  6559  sbthlemi5  6926  sbthlemi6  6927  updjud  7047  exmidfodomrlemim  7157  exmidaclem  7164  cc4f  7210  genpdisj  7464  ltexprlemloc  7548  recexprlemloc  7572  cauappcvgprlemrnd  7591  cauappcvgprlemdisj  7592  caucvgprlemrnd  7614  caucvgprlemdisj  7615  caucvgprprlemrnd  7642  caucvgprprlemdisj  7643  suplocexpr  7666  recan  11051  climconst  11231  sumeq2ad  11310  dvdsext  11793  zsupssdc  11887  pc11  12262  neif  12781  lmconst  12856  cndis  12881  2sqlem10  13601