Theorem ralrimivw 3134

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  r19.21v  3163  r19.37v  3164  r19.27v  3167  r19.28v  3169  2rmorex  3701  2reurex  3707  riinrab  5027  exse  5588  mpoeq12  7437  ovmpt3rabdm  7623  offveqb  7655  epweon  7726  exse2  7865  xpexgALT  7931  opabn1stprc  8008  mpoexg  8026  boxriin  8885  fisupg  9195  fisup2g  9379  fisupcl  9380  fiinfg  9411  fiinf2g  9412  ordtypelem8  9437  wemapso2  9465  cantnflem1  9607  r1val1  9707  updjud  9855  dfac12k  10067  compssiso  10293  axcclem  10376  ondomon  10482  tskuni  10703  pinq  10847  supexpr  10974  dedekind  11306  supadd  12121  supmullem2  12124  zsupss  12884  qextlt  13152  qextle  13153  xrsupsslem  13256  xrinfmsslem  13257  supxrpnf  13267  ssnn0fi  13944  recan  15296  climconst  15502  sumeq2sdvOLD  15663  dvdsext  16287  smupvallem  16449  smumullem  16458  pc11  16848  prmreclem4  16887  vdwmc2  16947  vdwlem8  16956  vdwlem13  16961  cshwsex  17068  cshws0  17069  prdsplusg  17418  prdsmulr  17419  prdsvsca  17420  prdshom  17427  imasplusg  17478  imasmulr  17479  imasip  17482  imasaddvallem  17490  imasvscaf  17500  quslem  17504  divsfval  17508  mrcuni  17584  catideu  17638  homfeqd  17658  comfeqd  17670  2oppccomf  17688  catcoppccl  18081  lublecllem  18321  chnfi  18597  pmtrrn  19429  pmtrfrn  19430  gsummptif1n0  19938  ip2eq  21649  frlmup4  21797  evlseu  22077  pmatcollpw2lem  22758  basdif0  22934  clsval2  23031  neif  23081  ordtbaslem  23169  ordtrest2lem  23184  lmconst  23242  cndis  23272  pnrmopn  23324  cmpfi  23389  finptfin  23499  comppfsc  23513  ptbasfi  23562  pttoponconst  23578  ptcnplem  23602  pthaus  23619  xkoptsub  23635  xkopt  23636  nrmr0reg  23730  ordthmeolem  23782  fbssfi  23818  filconn  23864  hausflim  23962  cnpflf  23982  fclscf  24006  cnpfcf  24022  alexsublem  24025  ptcmplem2  24034  ptcmplem3  24035  tsmsfbas  24109  eltsms  24114  utopbas  24216  isucn2  24259  psmetutop  24548  nrginvrcn  24673  lebnumlem3  24946  fmcfil  25255  ovolicc2lem4  25503  mbfconst  25616  i1fmul  25679  itg2const  25723  itg2cnlem2  25745  itgle  25793  ibladdlem  25803  iblabs  25812  iblabsr  25813  iblmulc2  25814  bddmulibl  25822  bddiblnc  25825  ellimc2  25860  limcnlp  25861  c1lip1  25980  itgpowd  26033  ply1nzb  26104  ulm0  26375  itgulm2  26393  dchrhash  27254  lgsquadlem2  27364  2sqlem10  27411  dchrisum  27475  rpvmasum2  27495  pntlemj  27586  bday0b  27825  axcontlem12  29064  nbgr0edg  29446  rusgr1vtx  29678  uspgr2wlkeq2  29736  clwwlknondisj  30202  ip2eqi  30948  ubthlem1  30962  hial2eq  31198  pjnmopi  32240  ssmd1  32403  chrelat2i  32457  xrofsup  32861  prodindf  32943  extdgfialglem2  33859  ordtrest2NEWlem  34088  truae  34409  mbfmcst  34425  mbfmcnt  34434  dya2iocuni  34449  0rrv  34617  hashreprin  34786  reprgt  34787  breprexplemc  34798  breprexp  34799  circlemeth  34806  hgt750lema  34823  fineqvnttrclselem1  35287  fineqvnttrclse  35290  vonf1owev  35312  wevgblacfn  35313  cvmliftlem15  35502  satf0suclem  35579  fmla0disjsuc  35602  fmlasucdisj  35603  neibastop2lem  36564  tailf  36579  filnetlem4  36585  fin2so  37950  matunitlindflem1  37959  matunitlindflem2  37960  poimirlem26  37989  poimirlem28  37991  ismblfin  38004  cnambfre  38011  itg2addnclem  38014  itg2addnc  38017  itg2gt0cn  38018  ibladdnclem  38019  iblabsnc  38027  iblmulc2nc  38028  ftc1anclem6  38041  ftc1anclem7  38042  ftc1anclem8  38043  ftc1anc  38044  frinfm  38078  sdclem1  38086  ssbnd  38131  rngoueqz  38283  lssatle  39483  ltrneq2  40616  tendoeq2  41242  lcmineqlem12  42501  hbtlem7  43579  trclrelexplem  44164  rfovcnvf1od  44457  dssmapf1od  44474  neik0pk1imk0  44500  collexd  44710  sswfaxreg  45440  omssaxinf2  45441  prodeq2ad  46048  0cnv  46196  itgperiod  46435  stoweidlem35  46489  stoweidlem59  46513  fourierdlem31  46592  subsaliuncllem  46811  subsaliuncl  46812  iundjiun  46914  hoiprodcl2  47009  ovn0lem  47019  hoidmvlelem3  47051  smflimlem1  47225  smflimlem2  47226  smflimlem3  47227  fundcmpsurinjlem2  47879  sprval  47959  prprval  47994  rmsupp0  48864  lincop  48904  lcoc0  48918  nelsubclem  49562