Theorem ralrimivw 2571

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  r19.27v  2624  r19.28v  2625  exse  4371  sosng  4736  dmxpm  4886  exse2  5043  funco  5298  acexmidlemph  5915  mpoeq12  5982  xpexgALT  6190  mpoexg  6269  rdgtfr  6432  rdgruledefgg  6433  rdgivallem  6439  frecabex  6456  frectfr  6458  omfnex  6507  oeiv  6514  uniqs  6652  exmidpw2en  6973  sbthlemi5  7027  sbthlemi6  7028  updjud  7148  exmidfodomrlemim  7268  exmidaclem  7275  exmidapne  7327  cc4f  7336  genpdisj  7590  ltexprlemloc  7674  recexprlemloc  7698  cauappcvgprlemrnd  7717  cauappcvgprlemdisj  7718  caucvgprlemrnd  7740  caucvgprlemdisj  7741  caucvgprprlemrnd  7768  caucvgprprlemdisj  7769  suplocexpr  7792  zsupssdc  10328  nninfinf  10535  recan  11274  climconst  11455  sumeq2ad  11534  dvdsext  12020  pc11  12500  ptex  12935  prdsex  12940  imasex  12948  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfnlemg  12957  imasaddvallemg  12958  quslem  12967  grpinvfng  13176  scaffng  13865  neif  14377  lmconst  14452  cndis  14477  plyval  14968  lgsquadlem2  15319  2sqlem10  15366