Theorem ralrimivw 2568

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

Syntax hints:   → wi 4   ∈ wcel 2164  ∀wral 2472

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 2477

This theorem is referenced by:  r19.27v  2621  r19.28v  2622  exse  4368  sosng  4733  dmxpm  4883  exse2  5040  funco  5295  acexmidlemph  5912  mpoeq12  5979  xpexgALT  6187  mpoexg  6266  rdgtfr  6429  rdgruledefgg  6430  rdgivallem  6436  frecabex  6453  frectfr  6455  omfnex  6504  oeiv  6511  uniqs  6649  exmidpw2en  6970  sbthlemi5  7022  sbthlemi6  7023  updjud  7143  exmidfodomrlemim  7263  exmidaclem  7270  exmidapne  7322  cc4f  7331  genpdisj  7585  ltexprlemloc  7669  recexprlemloc  7693  cauappcvgprlemrnd  7712  cauappcvgprlemdisj  7713  caucvgprlemrnd  7735  caucvgprlemdisj  7736  caucvgprprlemrnd  7763  caucvgprprlemdisj  7764  suplocexpr  7787  nninfinf  10517  recan  11256  climconst  11436  sumeq2ad  11515  dvdsext  12000  zsupssdc  12094  pc11  12472  ptex  12878  prdsex  12883  imasex  12891  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfnlemg  12900  imasaddvallemg  12901  quslem  12910  grpinvfng  13119  scaffng  13808  neif  14320  lmconst  14395  cndis  14420  plyval  14911  lgsquadlem2  15235  2sqlem10  15282