Theorem ralrimivw 2624

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  r19.27v  2678  r19.28v  2679  exse  4481  sosng  4848  dmxpm  5002  exse2  5161  funco  5417  acexmidlemph  6078  mpoeq12  6148  xpexgALT  6366  opabn1stprc  6429  mpoexg  6447  rdgtfr  6645  rdgruledefgg  6646  rdgivallem  6652  frecabex  6669  frectfr  6671  omfnex  6722  oeiv  6729  uniqs  6867  exmidpw2en  7219  exmidssfi  7246  sbthlemi5  7278  sbthlemi6  7279  updjud  7422  exmidfodomrlemim  7553  exmidaclem  7564  exmidapne  7626  cc4f  7635  genpdisj  7890  ltexprlemloc  7974  recexprlemloc  7998  cauappcvgprlemrnd  8017  cauappcvgprlemdisj  8018  caucvgprlemrnd  8040  caucvgprlemdisj  8041  caucvgprprlemrnd  8068  caucvgprprlemdisj  8069  suplocexpr  8092  zsupssdc  10673  nninfinf  10880  recan  11875  climconst  12056  sumeq2ad  12135  dvdsext  12622  pc11  13110  ptex  13618  imasex  13626  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfnlemg  13635  imasaddvallemg  13636  quslem  13645  grpinvfng  13849  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdsbas  14176  scaffng  14646  neif  15242  lmconst  15317  cndis  15342  plyval  15833  lgsquadlem2  16197  2sqlem10  16244  vtxdumgrfival  16539  uspgr2wlkeq2  16607  pw1dceq  17035  exmidnotnotr  17036  exmidcon  17037  exmidpeirce  17038  wexmiddiffi  17044  wexmiddifxy  17046