Theorem ralrimivw 2564

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

Syntax hints:   → wi 4   ∈ wcel 2160  ∀wral 2468

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  r19.27v  2617  r19.28v  2618  exse  4351  sosng  4714  dmxpm  4862  exse2  5017  funco  5271  acexmidlemph  5884  mpoeq12  5951  xpexgALT  6152  mpoexg  6230  rdgtfr  6393  rdgruledefgg  6394  rdgivallem  6400  frecabex  6417  frectfr  6419  omfnex  6468  oeiv  6475  uniqs  6611  sbthlemi5  6979  sbthlemi6  6980  updjud  7100  exmidfodomrlemim  7219  exmidaclem  7226  exmidapne  7278  cc4f  7287  genpdisj  7541  ltexprlemloc  7625  recexprlemloc  7649  cauappcvgprlemrnd  7668  cauappcvgprlemdisj  7669  caucvgprlemrnd  7691  caucvgprlemdisj  7692  caucvgprprlemrnd  7719  caucvgprprlemdisj  7720  suplocexpr  7743  recan  11137  climconst  11317  sumeq2ad  11396  dvdsext  11880  zsupssdc  11974  pc11  12349  ptex  12741  prdsex  12746  imasex  12754  imasbas  12756  imasplusg  12757  imasmulr  12758  imasaddfnlemg  12763  imasaddvallemg  12764  quslem  12773  grpinvfng  12960  scaffng  13592  neif  14044  lmconst  14119  cndis  14144  2sqlem10  14875