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  4372  sosng  4737  dmxpm  4887  exse2  5044  funco  5299  acexmidlemph  5918  mpoeq12  5986  xpexgALT  6199  mpoexg  6278  rdgtfr  6441  rdgruledefgg  6442  rdgivallem  6448  frecabex  6465  frectfr  6467  omfnex  6516  oeiv  6523  uniqs  6661  exmidpw2en  6982  sbthlemi5  7036  sbthlemi6  7037  updjud  7157  exmidfodomrlemim  7280  exmidaclem  7291  exmidapne  7343  cc4f  7352  genpdisj  7607  ltexprlemloc  7691  recexprlemloc  7715  cauappcvgprlemrnd  7734  cauappcvgprlemdisj  7735  caucvgprlemrnd  7757  caucvgprlemdisj  7758  caucvgprprlemrnd  7785  caucvgprprlemdisj  7786  suplocexpr  7809  zsupssdc  10345  nninfinf  10552  recan  11291  climconst  11472  sumeq2ad  11551  dvdsext  12037  pc11  12525  ptex  12966  prdsex  12971  prdsval  12975  prdsbaslemss  12976  prdsbas  12978  imasex  13007  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfnlemg  13016  imasaddvallemg  13017  quslem  13026  grpinvfng  13246  scaffng  13941  neif  14461  lmconst  14536  cndis  14561  plyval  15052  lgsquadlem2  15403  2sqlem10  15450