Theorem ralrimivw 2618

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

Syntax hints:   → wi 4   ∈ wcel 2205  ∀wral 2522

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  r19.27v  2672  r19.28v  2673  exse  4459  sosng  4825  dmxpm  4979  exse2  5138  funco  5394  acexmidlemph  6045  mpoeq12  6115  xpexgALT  6328  opabn1stprc  6391  mpoexg  6409  rdgtfr  6607  rdgruledefgg  6608  rdgivallem  6614  frecabex  6631  frectfr  6633  omfnex  6684  oeiv  6691  uniqs  6829  exmidpw2en  7174  exmidssfi  7201  sbthlemi5  7233  sbthlemi6  7234  updjud  7375  exmidfodomrlemim  7506  exmidaclem  7517  exmidapne  7576  cc4f  7585  genpdisj  7840  ltexprlemloc  7924  recexprlemloc  7948  cauappcvgprlemrnd  7967  cauappcvgprlemdisj  7968  caucvgprlemrnd  7990  caucvgprlemdisj  7991  caucvgprprlemrnd  8018  caucvgprprlemdisj  8019  suplocexpr  8042  zsupssdc  10602  nninfinf  10809  recan  11798  climconst  11979  sumeq2ad  12058  dvdsext  12545  pc11  13033  ptex  13494  prdsex  13499  prdsval  13503  prdsbaslemss  13504  prdsbas  13506  imasex  13535  imasbas  13537  imasplusg  13538  imasmulr  13539  imasaddfnlemg  13544  imasaddvallemg  13545  quslem  13554  grpinvfng  13774  scaffng  14474  neif  15023  lmconst  15098  cndis  15123  plyval  15614  lgsquadlem2  15968  2sqlem10  16015  vtxdumgrfival  16310  uspgr2wlkeq2  16378  pw1dceq  16795  exmidnotnotr  16796  exmidcon  16797  exmidpeirce  16798