Theorem ralrimivw 3181

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3136

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

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

This theorem is referenced by:  r19.27v  3182  r19.28v  3184  r19.37v  3342  2rmorex  3743  2reurex  3748  riinrab  4997  exse  5512  dmxp  5792  mpoeq12  7219  ovmpt3rabdm  7396  offveqb  7423  exse2  7614  xpexgALT  7674  opabn1stprc  7748  mpoexg  7766  uniqs  8349  boxriin  8496  fisupg  8758  fisup2g  8924  fisupcl  8925  fiinfg  8955  fiinf2g  8956  ordtypelem8  8981  wemapso2  9009  cantnflem1  9144  r1val1  9207  scottex  9306  updjud  9355  dfac12k  9565  compssiso  9788  axcclem  9871  ondomon  9977  tskuni  10197  pinq  10341  supexpr  10468  dedekind  10795  supadd  11601  supmullem2  11604  zsupss  12329  qextlt  12588  qextle  12589  xrsupsslem  12692  xrinfmsslem  12693  supxrpnf  12703  ssnn0fi  13345  recan  14688  climconst  14892  sumeq2sdv  15053  dvdsext  15663  smupvallem  15824  smumullem  15833  pc11  16208  prmreclem4  16247  vdwmc2  16307  vdwlem8  16316  vdwlem13  16321  cshwsex  16426  cshws0  16427  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdshom  16732  imasplusg  16782  imasmulr  16783  imasip  16786  imasaddvallem  16794  imasvscaf  16804  quslem  16808  divsfval  16812  mrcuni  16884  catideu  16938  homfeqd  16957  comfeqd  16969  2oppccomf  16987  catcoppccl  17360  lublecllem  17590  pmtrrn  18577  pmtrfrn  18578  gsummptif1n0  19078  evlseu  20288  ip2eq  20789  frlmup4  20937  pmatcollpw2lem  21377  basdif0  21553  clsval2  21650  neif  21700  ordtbaslem  21788  ordtrest2lem  21803  lmconst  21861  cndis  21891  pnrmopn  21943  cmpfi  22008  finptfin  22118  comppfsc  22132  ptbasfi  22181  pttoponconst  22197  ptcnplem  22221  pthaus  22238  xkoptsub  22254  xkopt  22255  nrmr0reg  22349  ordthmeolem  22401  fbssfi  22437  filconn  22483  hausflim  22581  cnpflf  22601  fclscf  22625  cnpfcf  22641  alexsublem  22644  ptcmplem2  22653  ptcmplem3  22654  tsmsfbas  22728  eltsms  22733  utopbas  22836  isucn2  22880  psmetutop  23169  nrginvrcn  23293  lebnumlem3  23559  fmcfil  23867  ovolicc2lem4  24113  mbfconst  24226  i1fmul  24289  itg2const  24333  itg2cnlem2  24355  itgle  24402  ibladdlem  24412  iblabs  24421  iblabsr  24422  iblmulc2  24423  bddmulibl  24431  ellimc2  24467  limcnlp  24468  c1lip1  24586  ply1nzb  24708  ulm0  24971  itgulm2  24989  dchrhash  25839  lgsquadlem2  25949  2sqlem10  25996  dchrisum  26060  rpvmasum2  26080  pntlemj  26171  axcontlem12  26753  nbgr0edg  27131  rusgr1vtx  27362  uspgr2wlkeq2  27420  clwwlknondisj  27882  ip2eqi  28625  ubthlem1  28639  hial2eq  28875  occon  29056  spanss  29117  pjnmopi  29917  ssmd1  30080  chrelat2i  30134  xrofsup  30484  ordtrest2NEWlem  31158  prodindf  31275  truae  31495  mbfmcst  31510  mbfmcnt  31519  dya2iocuni  31534  0rrv  31702  hashreprin  31884  reprgt  31885  breprexplemc  31896  breprexp  31897  circlemeth  31904  hgt750lema  31921  cvmliftlem15  32538  satf0suclem  32615  fmla0disjsuc  32638  fmlasucdisj  32639  trpredss  33061  neibastop2lem  33701  tailf  33716  filnetlem4  33722  fin2so  34871  matunitlindflem1  34880  matunitlindflem2  34881  poimirlem26  34910  poimirlem28  34912  ismblfin  34925  cnambfre  34932  itg2addnclem  34935  itg2addnc  34938  itg2gt0cn  34939  ibladdnclem  34940  iblabsnc  34948  iblmulc2nc  34949  bddiblnc  34954  ftc1anclem6  34964  ftc1anclem7  34965  ftc1anclem8  34966  ftc1anc  34967  frinfm  35002  sdclem1  35010  ssbnd  35058  rngoueqz  35210  lssatle  36143  ltrneq2  37276  tendoeq2  37902  hbtlem7  39715  itgoss  39753  itgpowd  39811  trclrelexplem  40046  rfovcnvf1od  40340  dssmapf1od  40357  neik0pk1imk0  40387  collexd  40583  prodeq2ad  41862  0cnv  42012  itgperiod  42255  stoweidlem35  42310  stoweidlem59  42334  fourierdlem31  42413  subsaliuncllem  42630  subsaliuncl  42631  iundjiun  42732  hoiprodcl2  42827  ovnsslelem  42832  ovn0lem  42837  hoidmvlelem3  42869  smflimlem1  43037  smflimlem2  43038  smflimlem3  43039  fundcmpsurinjlem2  43549  sprval  43631  prprval  43666  rmsupp0  44406  lincop  44453  lcoc0  44467