Theorem ralrimivw 2561

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

Syntax hints:   → wi 4   ∈ wcel 2158  ∀wral 2465

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470

This theorem is referenced by:  r19.27v  2614  r19.28v  2615  exse  4348  sosng  4711  dmxpm  4859  exse2  5014  funco  5268  acexmidlemph  5881  mpoeq12  5948  xpexgALT  6147  mpoexg  6225  rdgtfr  6388  rdgruledefgg  6389  rdgivallem  6395  frecabex  6412  frectfr  6414  omfnex  6463  oeiv  6470  uniqs  6606  sbthlemi5  6973  sbthlemi6  6974  updjud  7094  exmidfodomrlemim  7213  exmidaclem  7220  exmidapne  7272  cc4f  7281  genpdisj  7535  ltexprlemloc  7619  recexprlemloc  7643  cauappcvgprlemrnd  7662  cauappcvgprlemdisj  7663  caucvgprlemrnd  7685  caucvgprlemdisj  7686  caucvgprprlemrnd  7713  caucvgprprlemdisj  7714  suplocexpr  7737  recan  11131  climconst  11311  sumeq2ad  11390  dvdsext  11874  zsupssdc  11968  pc11  12343  ptex  12730  prdsex  12735  imasex  12743  imasbas  12745  imasplusg  12746  imasmulr  12747  imasaddfnlemg  12752  imasaddvallemg  12753  quslem  12762  grpinvfng  12938  scaffng  13462  neif  13881  lmconst  13956  cndis  13981  2sqlem10  14712