Theorem ralrimivw 2478

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

Syntax hints:   → wi 4   ∈ wcel 1461  ∀wral 2388

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-ral 2393

This theorem is referenced by:  r19.27v  2531  r19.28v  2532  exse  4216  sosng  4570  dmxpm  4717  exse2  4869  funco  5119  acexmidlemph  5719  mpoeq12  5783  xpexgALT  5983  mpoexg  6061  rdgtfr  6223  rdgruledefgg  6224  rdgivallem  6230  frecabex  6247  frectfr  6249  omfnex  6297  oeiv  6304  uniqs  6439  sbthlemi5  6799  sbthlemi6  6800  updjud  6917  exmidfodomrlemim  7002  exmidaclem  7009  genpdisj  7273  ltexprlemloc  7357  recexprlemloc  7381  cauappcvgprlemrnd  7400  cauappcvgprlemdisj  7401  caucvgprlemrnd  7423  caucvgprlemdisj  7424  caucvgprprlemrnd  7451  caucvgprprlemdisj  7452  recan  10767  climconst  10945  sumeq2ad  11024  dvdsext  11395  neif  12147  lmconst  12221  cndis  12246