Theorem ralrimivw 2506

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

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

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 2421

This theorem is referenced by:  r19.27v  2559  r19.28v  2560  exse  4258  sosng  4612  dmxpm  4759  exse2  4913  funco  5163  acexmidlemph  5767  mpoeq12  5831  xpexgALT  6031  mpoexg  6109  rdgtfr  6271  rdgruledefgg  6272  rdgivallem  6278  frecabex  6295  frectfr  6297  omfnex  6345  oeiv  6352  uniqs  6487  sbthlemi5  6849  sbthlemi6  6850  updjud  6967  exmidfodomrlemim  7057  exmidaclem  7064  genpdisj  7331  ltexprlemloc  7415  recexprlemloc  7439  cauappcvgprlemrnd  7458  cauappcvgprlemdisj  7459  caucvgprlemrnd  7481  caucvgprlemdisj  7482  caucvgprprlemrnd  7509  caucvgprprlemdisj  7510  suplocexpr  7533  recan  10881  climconst  11059  sumeq2ad  11138  dvdsext  11553  neif  12310  lmconst  12385  cndis  12410