Theorem ralrimivw 3129

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  r19.21v  3158  r19.37v  3159  r19.27v  3164  r19.28v  3166  2rmorex  3722  2reurex  3728  riinrab  5043  exse  5591  mpoeq12  7442  ovmpt3rabdm  7628  offveqb  7660  epweon  7731  exse2  7873  xpexgALT  7939  opabn1stprc  8016  mpoexg  8034  boxriin  8890  fisupg  9211  fisup2g  9396  fisupcl  9397  fiinfg  9428  fiinf2g  9429  ordtypelem8  9454  wemapso2  9482  cantnflem1  9620  r1val1  9717  updjud  9865  dfac12k  10079  compssiso  10305  axcclem  10388  ondomon  10494  tskuni  10714  pinq  10858  supexpr  10985  dedekind  11315  supadd  12129  supmullem2  12132  zsupss  12874  qextlt  13141  qextle  13142  xrsupsslem  13245  xrinfmsslem  13246  supxrpnf  13256  ssnn0fi  13928  recan  15280  climconst  15486  sumeq2sdvOLD  15647  dvdsext  16268  smupvallem  16430  smumullem  16439  pc11  16828  prmreclem4  16867  vdwmc2  16927  vdwlem8  16936  vdwlem13  16941  cshwsex  17048  cshws0  17049  prdsplusg  17398  prdsmulr  17399  prdsvsca  17400  prdshom  17407  imasplusg  17457  imasmulr  17458  imasip  17461  imasaddvallem  17469  imasvscaf  17479  quslem  17483  divsfval  17487  mrcuni  17563  catideu  17617  homfeqd  17637  comfeqd  17649  2oppccomf  17667  catcoppccl  18060  lublecllem  18300  pmtrrn  19372  pmtrfrn  19373  gsummptif1n0  19881  ip2eq  21596  frlmup4  21744  evlseu  22024  pmatcollpw2lem  22698  basdif0  22874  clsval2  22971  neif  23021  ordtbaslem  23109  ordtrest2lem  23124  lmconst  23182  cndis  23212  pnrmopn  23264  cmpfi  23329  finptfin  23439  comppfsc  23453  ptbasfi  23502  pttoponconst  23518  ptcnplem  23542  pthaus  23559  xkoptsub  23575  xkopt  23576  nrmr0reg  23670  ordthmeolem  23722  fbssfi  23758  filconn  23804  hausflim  23902  cnpflf  23922  fclscf  23946  cnpfcf  23962  alexsublem  23965  ptcmplem2  23974  ptcmplem3  23975  tsmsfbas  24049  eltsms  24054  utopbas  24157  isucn2  24200  psmetutop  24489  nrginvrcn  24614  lebnumlem3  24896  fmcfil  25206  ovolicc2lem4  25455  mbfconst  25568  i1fmul  25631  itg2const  25675  itg2cnlem2  25697  itgle  25745  ibladdlem  25755  iblabs  25764  iblabsr  25765  iblmulc2  25766  bddmulibl  25774  bddiblnc  25777  ellimc2  25812  limcnlp  25813  c1lip1  25936  itgpowd  25991  ply1nzb  26062  ulm0  26334  itgulm2  26352  dchrhash  27216  lgsquadlem2  27326  2sqlem10  27373  dchrisum  27437  rpvmasum2  27457  pntlemj  27548  bday0b  27780  axcontlem12  28956  nbgr0edg  29338  rusgr1vtx  29570  uspgr2wlkeq2  29628  clwwlknondisj  30091  ip2eqi  30836  ubthlem1  30850  hial2eq  31086  pjnmopi  32128  ssmd1  32291  chrelat2i  32345  xrofsup  32741  prodindf  32837  ordtrest2NEWlem  33906  truae  34227  mbfmcst  34244  mbfmcnt  34253  dya2iocuni  34268  0rrv  34436  hashreprin  34605  reprgt  34606  breprexplemc  34617  breprexp  34618  circlemeth  34625  hgt750lema  34642  vonf1owev  35089  wevgblacfn  35090  cvmliftlem15  35279  satf0suclem  35356  fmla0disjsuc  35379  fmlasucdisj  35380  neibastop2lem  36342  tailf  36357  filnetlem4  36363  fin2so  37595  matunitlindflem1  37604  matunitlindflem2  37605  poimirlem26  37634  poimirlem28  37636  ismblfin  37649  cnambfre  37656  itg2addnclem  37659  itg2addnc  37662  itg2gt0cn  37663  ibladdnclem  37664  iblabsnc  37672  iblmulc2nc  37673  ftc1anclem6  37686  ftc1anclem7  37687  ftc1anclem8  37688  ftc1anc  37689  frinfm  37723  sdclem1  37731  ssbnd  37776  rngoueqz  37928  lssatle  39002  ltrneq2  40136  tendoeq2  40762  lcmineqlem12  42022  hbtlem7  43108  trclrelexplem  43694  rfovcnvf1od  43987  dssmapf1od  44004  neik0pk1imk0  44030  collexd  44240  sswfaxreg  44971  omssaxinf2  44972  prodeq2ad  45584  0cnv  45734  itgperiod  45973  stoweidlem35  46027  stoweidlem59  46051  fourierdlem31  46130  subsaliuncllem  46349  subsaliuncl  46350  iundjiun  46452  hoiprodcl2  46547  ovn0lem  46557  hoidmvlelem3  46589  smflimlem1  46763  smflimlem2  46764  smflimlem3  46765  fundcmpsurinjlem2  47394  sprval  47474  prprval  47509  rmsupp0  48350  lincop  48391  lcoc0  48405  nelsubclem  49050