Theorem ralrimivw 3137

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 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 3132	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-ral 3056

This theorem is referenced by:  r19.21v  3166  r19.37v  3167  r19.27v  3170  r19.28v  3172  2rmorex  3697  2reurex  3703  riinrab  5016  exse  5581  mpoeq12  7433  ovmpt3rabdm  7619  offveqb  7651  epweon  7722  exse2  7861  xpexgALT  7927  opabn1stprc  8004  mpoexg  8022  boxriin  8882  fisupg  9192  fisup2g  9376  fisupcl  9377  fiinfg  9408  fiinf2g  9409  ordtypelem8  9434  wemapso2  9462  cantnflem1  9605  r1val1  9705  updjud  9853  dfac12k  10065  compssiso  10291  axcclem  10374  ondomon  10480  tskuni  10701  pinq  10845  supexpr  10972  dedekind  11304  supadd  12119  supmullem2  12122  zsupss  12882  qextlt  13150  qextle  13151  xrsupsslem  13254  xrinfmsslem  13255  supxrpnf  13265  ssnn0fi  13942  recan  15294  climconst  15500  sumeq2sdvOLD  15661  dvdsext  16285  smupvallem  16447  smumullem  16456  pc11  16846  prmreclem4  16885  vdwmc2  16945  vdwlem8  16954  vdwlem13  16959  cshwsex  17066  cshws0  17067  prdsplusg  17416  prdsmulr  17417  prdsvsca  17418  prdshom  17425  imasplusg  17476  imasmulr  17477  imasip  17480  imasaddvallem  17488  imasvscaf  17498  quslem  17502  divsfval  17506  mrcuni  17582  catideu  17636  homfeqd  17656  comfeqd  17668  2oppccomf  17686  catcoppccl  18079  lublecllem  18319  chnfi  18595  pmtrrn  19427  pmtrfrn  19428  gsummptif1n0  19936  ip2eq  21632  frlmup4  21780  evlseu  22063  pmatcollpw2lem  22764  basdif0  22940  clsval2  23037  neif  23087  ordtbaslem  23175  ordtrest2lem  23190  lmconst  23248  cndis  23278  pnrmopn  23330  cmpfi  23395  finptfin  23505  comppfsc  23519  ptbasfi  23568  pttoponconst  23584  ptcnplem  23608  pthaus  23625  xkoptsub  23641  xkopt  23642  nrmr0reg  23736  ordthmeolem  23788  fbssfi  23824  filconn  23870  hausflim  23968  cnpflf  23988  fclscf  24012  cnpfcf  24028  alexsublem  24031  ptcmplem2  24040  ptcmplem3  24041  tsmsfbas  24115  eltsms  24120  utopbas  24222  isucn2  24265  psmetutop  24554  nrginvrcn  24679  lebnumlem3  24952  fmcfil  25261  ovolicc2lem4  25509  mbfconst  25622  i1fmul  25685  itg2const  25729  itg2cnlem2  25751  itgle  25799  ibladdlem  25809  iblabs  25818  iblabsr  25819  iblmulc2  25820  bddmulibl  25828  bddiblnc  25831  ellimc2  25866  limcnlp  25867  c1lip1  25986  itgpowd  26039  ply1nzb  26110  ulm0  26378  itgulm2  26396  dchrhash  27256  lgsquadlem2  27366  2sqlem10  27413  dchrisum  27477  rpvmasum2  27497  pntlemj  27588  bday0b  27827  axcontlem12  29066  nbgr0edg  29448  rusgr1vtx  29679  uspgr2wlkeq2  29737  clwwlknondisj  30203  ip2eqi  30949  ubthlem1  30963  hial2eq  31199  pjnmopi  32241  ssmd1  32404  chrelat2i  32458  xrofsup  32863  prodindf  32945  selvply1rhmlemb  33715  extdgfialglem2  33889  ordtrest2NEWlem  34118  truae  34439  mbfmcst  34455  mbfmcnt  34464  dya2iocuni  34479  0rrv  34647  hashreprin  34816  reprgt  34817  breprexplemc  34828  breprexp  34829  circlemeth  34836  hgt750lema  34853  fineqvnttrclselem1  35317  fineqvnttrclse  35320  vonf1owev  35351  wevgblacfn  35352  cvmliftlem15  35541  satf0suclem  35618  fmla0disjsuc  35641  fmlasucdisj  35642  neibastop2lem  36603  tailf  36618  filnetlem4  36624  fin2so  37989  matunitlindflem1  37998  matunitlindflem2  37999  poimirlem26  38028  poimirlem28  38030  ismblfin  38043  cnambfre  38050  itg2addnclem  38053  itg2addnc  38056  itg2gt0cn  38057  ibladdnclem  38058  iblabsnc  38066  iblmulc2nc  38067  ftc1anclem6  38080  ftc1anclem7  38081  ftc1anclem8  38082  ftc1anc  38083  frinfm  38117  sdclem1  38125  ssbnd  38170  rngoueqz  38322  lssatle  39522  ltrneq2  40655  tendoeq2  41281  lcmineqlem12  42540  hbtlem7  43585  trclrelexplem  44170  rfovcnvf1od  44463  dssmapf1od  44480  neik0pk1imk0  44506  collexd  44716  sswfaxreg  45446  omssaxinf2  45447  prodeq2ad  46051  0cnv  46199  itgperiod  46438  stoweidlem35  46492  stoweidlem59  46516  fourierdlem31  46595  subsaliuncllem  46814  subsaliuncl  46815  iundjiun  46917  hoiprodcl2  47012  ovn0lem  47022  hoidmvlelem3  47054  smflimlem1  47228  smflimlem2  47229  smflimlem3  47230  fundcmpsurinjlem2  47888  sprval  47968  prprval  48003  rmsupp0  48873  lincop  48913  lcoc0  48927  nelsubclem  49571