Theorem ralrimivw 3160

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

Syntax hints:   → wi 4   ∈ wcel 2144  ∀wral 3078

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

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

This theorem is referenced by:  r19.21v  3189  r19.37v  3190  r19.27v  3193  r19.28v  3195  2rmorex  3719  2reurex  3725  riinrab  5043  exse  5609  mpoeq12  7471  ovmpt3rabdm  7657  offveqb  7689  epweon  7760  exse2  7900  xpexgALT  7964  opabn1stprc  8041  mpoexg  8059  boxriin  8924  fisupg  9234  fisup2g  9417  fisupcl  9418  fiinfg  9449  fiinf2g  9450  ordtypelem8  9475  wemapso2  9503  cantnflem1  9646  r1val1  9746  updjud  9894  dfac12k  10106  compssiso  10333  axcclem  10416  ondomon  10522  tskuni  10743  pinq  10887  supexpr  11014  dedekind  11348  supadd  12162  supmullem2  12165  zsupss  12940  qextlt  13208  qextle  13209  xrsupsslem  13312  xrinfmsslem  13313  supxrpnf  13323  ssnn0fi  14000  recan  15366  climconst  15572  sumeq2sdvOLD  15733  dvdsext  16357  smupvallem  16519  smumullem  16528  pc11  16918  prmreclem4  16957  vdwmc2  17017  vdwlem8  17026  vdwlem13  17031  cshwsex  17138  cshws0  17139  prdsplusg  17489  prdsmulr  17490  prdsvsca  17491  prdshom  17498  imasplusg  17549  imasmulr  17550  imasip  17553  imasaddvallem  17561  imasvscaf  17571  quslem  17575  divsfval  17579  mrcuni  17655  catideu  17709  homfeqd  17729  comfeqd  17741  2oppccomf  17759  catcoppccl  18152  lublecllem  18392  chnfi  18668  pmtrrn  19499  pmtrfrn  19500  gsummptif1n0  20008  ip2eq  21707  frlmup4  21855  evlseu  22138  pmatcollpw2lem  22839  basdif0  23015  clsval2  23112  neif  23162  ordtbaslem  23250  ordtrest2lem  23265  lmconst  23323  cndis  23353  pnrmopn  23405  cmpfi  23470  finptfin  23580  comppfsc  23594  ptbasfi  23643  pttoponconst  23659  ptcnplem  23683  pthaus  23700  xkoptsub  23716  xkopt  23717  nrmr0reg  23811  ordthmeolem  23863  fbssfi  23899  filconn  23945  hausflim  24043  cnpflf  24063  fclscf  24087  cnpfcf  24103  alexsublem  24106  ptcmplem2  24115  ptcmplem3  24116  tsmsfbas  24190  eltsms  24195  utopbas  24297  isucn2  24340  psmetutop  24629  nrginvrcn  24754  lebnumlem3  25027  fmcfil  25336  ovolicc2lem4  25584  mbfconst  25697  i1fmul  25760  itg2const  25804  itg2cnlem2  25826  itgle  25874  ibladdlem  25884  iblabs  25893  iblabsr  25894  iblmulc2  25895  bddmulibl  25903  bddiblnc  25906  ellimc2  25941  limcnlp  25942  c1lip1  26061  itgpowd  26114  ply1nzb  26185  ulm0  26456  itgulm2  26474  dchrhash  27337  lgsquadlem2  27447  2sqlem10  27494  dchrisum  27558  rpvmasum2  27578  pntlemj  27669  bday0b  27908  axcontlem12  29178  nbgr0edg  29560  rusgr1vtx  29791  uspgr2wlkeq2  29849  clwwlknondisj  30315  ip2eqi  31061  ubthlem1  31075  hial2eq  31311  pjnmopi  32353  ssmd1  32516  chrelat2i  32570  xrofsup  32971  prodindf  33042  selvply1rhmlemb  33818  extdgfialglem2  33992  ordtrest2NEWlem  34221  truae  34542  mbfmcst  34558  mbfmcnt  34567  dya2iocuni  34582  0rrv  34750  hashreprin  34916  reprgt  34917  breprexplemc  34928  breprexp  34929  circlemeth  34936  hgt750lema  34953  fineqvnttrclselem1  35421  fineqvnttrclse  35424  vonf1wev  35455  vonf1owevOLD  35457  wevgblacfn  35458  onvfowev  35463  cvmliftlem15  35653  satf0suclem  35730  fmla0disjsuc  35753  fmlasucdisj  35754  neibastop2lem  36725  tailf  36740  filnetlem4  36746  fin2so  38111  matunitlindflem1  38120  matunitlindflem2  38121  poimirlem26  38150  poimirlem28  38152  ismblfin  38165  cnambfre  38172  itg2addnclem  38175  itg2addnc  38178  itg2gt0cn  38179  ibladdnclem  38180  iblabsnc  38188  iblmulc2nc  38189  ftc1anclem6  38202  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  frinfm  38239  sdclem1  38247  ssbnd  38292  rngoueqz  38444  lssatle  39644  ltrneq2  40777  tendoeq2  41403  lcmineqlem12  42662  hbtlem7  43707  trclrelexplem  44292  rfovcnvf1od  44585  dssmapf1od  44602  neik0pk1imk0  44628  collexd  44838  sswfaxreg  45568  omssaxinf2  45569  prodeq2ad  46173  0cnv  46321  itgperiod  46560  stoweidlem35  46614  stoweidlem59  46638  fourierdlem31  46717  subsaliuncllem  46936  subsaliuncl  46937  iundjiun  47039  hoiprodcl2  47134  ovn0lem  47144  hoidmvlelem3  47176  smflimlem1  47350  smflimlem2  47351  smflimlem3  47352  fundcmpsurinjlem2  48010  sprval  48090  prprval  48125  rmsupp0  48995  lincop  49035  lcoc0  49049  nelsubclem  49693