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  7423  exmidfodomrlemim  7554  exmidaclem  7565  exmidapne  7627  cc4f  7636  genpdisj  7891  ltexprlemloc  7975  recexprlemloc  7999  cauappcvgprlemrnd  8018  cauappcvgprlemdisj  8019  caucvgprlemrnd  8041  caucvgprlemdisj  8042  caucvgprprlemrnd  8069  caucvgprprlemdisj  8070  suplocexpr  8093  zsupssdc  10684  nninfinf  10895  recan  11892  climconst  12075  sumeq2ad  12154  dvdsext  12641  pc11  13133  ptex  13671  imasex  13679  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfnlemg  13688  imasaddvallemg  13689  quslem  13698  grpinvfng  13902  prdsex  14263  prdsval  14264  prdsbaslemss  14265  prdsbas  14267  scaffng  14737  neif  15341  lmconst  15416  cndis  15441  plyval  15932  lgsquadlem2  16376  2sqlem10  16423  vtxdumgrfival  16718  uspgr2wlkeq2  16786  pw1dceq  17214  exmidnotnotr  17215  exmidcon  17216  exmidpeirce  17217  wexmiddiffi  17223  wexmiddifxy  17225