Theorem ralrimivw 2549

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

Syntax hints:   → wi 4   ∈ wcel 2146  ∀wral 2453

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458

This theorem is referenced by:  r19.27v  2602  r19.28v  2603  exse  4330  sosng  4693  dmxpm  4840  exse2  4995  funco  5248  acexmidlemph  5858  mpoeq12  5925  xpexgALT  6124  mpoexg  6202  rdgtfr  6365  rdgruledefgg  6366  rdgivallem  6372  frecabex  6389  frectfr  6391  omfnex  6440  oeiv  6447  uniqs  6583  sbthlemi5  6950  sbthlemi6  6951  updjud  7071  exmidfodomrlemim  7190  exmidaclem  7197  cc4f  7243  genpdisj  7497  ltexprlemloc  7581  recexprlemloc  7605  cauappcvgprlemrnd  7624  cauappcvgprlemdisj  7625  caucvgprlemrnd  7647  caucvgprlemdisj  7648  caucvgprprlemrnd  7675  caucvgprprlemdisj  7676  suplocexpr  7699  recan  11086  climconst  11266  sumeq2ad  11345  dvdsext  11828  zsupssdc  11922  pc11  12297  grpinvfng  12788  neif  13221  lmconst  13296  cndis  13321  2sqlem10  14041