Theorem ralrimivw 2504

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

Syntax hints:   → wi 4   ∈ wcel 1480  ∀wral 2414

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419

This theorem is referenced by:  r19.27v  2557  r19.28v  2558  exse  4253  sosng  4607  dmxpm  4754  exse2  4908  funco  5158  acexmidlemph  5760  mpoeq12  5824  xpexgALT  6024  mpoexg  6102  rdgtfr  6264  rdgruledefgg  6265  rdgivallem  6271  frecabex  6288  frectfr  6290  omfnex  6338  oeiv  6345  uniqs  6480  sbthlemi5  6842  sbthlemi6  6843  updjud  6960  exmidfodomrlemim  7050  exmidaclem  7057  genpdisj  7324  ltexprlemloc  7408  recexprlemloc  7432  cauappcvgprlemrnd  7451  cauappcvgprlemdisj  7452  caucvgprlemrnd  7474  caucvgprlemdisj  7475  caucvgprprlemrnd  7502  caucvgprprlemdisj  7503  suplocexpr  7526  recan  10874  climconst  11052  sumeq2ad  11131  dvdsext  11542  neif  12299  lmconst  12374  cndis  12399