Theorem ralrimivw 3150

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3061

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 3062

This theorem is referenced by:  r19.21v  3180  r19.37v  3182  r19.27v  3188  r19.28v  3190  2rmorex  3760  2reurex  3766  riinrab  5084  exse  5645  dmxpOLD  5940  mpoeq12  7506  ovmpt3rabdm  7692  offveqb  7724  epweon  7795  exse2  7939  xpexgALT  8006  opabn1stprc  8083  mpoexg  8101  uniqs  8817  boxriin  8980  fisupg  9324  fisup2g  9508  fisupcl  9509  fiinfg  9539  fiinf2g  9540  ordtypelem8  9565  wemapso2  9593  cantnflem1  9729  r1val1  9826  updjud  9974  dfac12k  10188  compssiso  10414  axcclem  10497  ondomon  10603  tskuni  10823  pinq  10967  supexpr  11094  dedekind  11424  supadd  12236  supmullem2  12239  zsupss  12979  qextlt  13245  qextle  13246  xrsupsslem  13349  xrinfmsslem  13350  supxrpnf  13360  ssnn0fi  14026  recan  15375  climconst  15579  sumeq2sdvOLD  15740  dvdsext  16358  smupvallem  16520  smumullem  16529  pc11  16918  prmreclem4  16957  vdwmc2  17017  vdwlem8  17026  vdwlem13  17031  cshwsex  17138  cshws0  17139  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdshom  17512  imasplusg  17562  imasmulr  17563  imasip  17566  imasaddvallem  17574  imasvscaf  17584  quslem  17588  divsfval  17592  mrcuni  17664  catideu  17718  homfeqd  17738  comfeqd  17750  2oppccomf  17768  catcoppccl  18162  lublecllem  18405  pmtrrn  19475  pmtrfrn  19476  gsummptif1n0  19984  ip2eq  21671  frlmup4  21821  evlseu  22107  pmatcollpw2lem  22783  basdif0  22960  clsval2  23058  neif  23108  ordtbaslem  23196  ordtrest2lem  23211  lmconst  23269  cndis  23299  pnrmopn  23351  cmpfi  23416  finptfin  23526  comppfsc  23540  ptbasfi  23589  pttoponconst  23605  ptcnplem  23629  pthaus  23646  xkoptsub  23662  xkopt  23663  nrmr0reg  23757  ordthmeolem  23809  fbssfi  23845  filconn  23891  hausflim  23989  cnpflf  24009  fclscf  24033  cnpfcf  24049  alexsublem  24052  ptcmplem2  24061  ptcmplem3  24062  tsmsfbas  24136  eltsms  24141  utopbas  24244  isucn2  24288  psmetutop  24580  nrginvrcn  24713  lebnumlem3  24995  fmcfil  25306  ovolicc2lem4  25555  mbfconst  25668  i1fmul  25731  itg2const  25775  itg2cnlem2  25797  itgle  25845  ibladdlem  25855  iblabs  25864  iblabsr  25865  iblmulc2  25866  bddmulibl  25874  bddiblnc  25877  ellimc2  25912  limcnlp  25913  c1lip1  26036  itgpowd  26091  ply1nzb  26162  ulm0  26434  itgulm2  26452  dchrhash  27315  lgsquadlem2  27425  2sqlem10  27472  dchrisum  27536  rpvmasum2  27556  pntlemj  27647  bday0b  27875  axcontlem12  28990  nbgr0edg  29374  rusgr1vtx  29606  uspgr2wlkeq2  29665  clwwlknondisj  30130  ip2eqi  30875  ubthlem1  30889  hial2eq  31125  pjnmopi  32167  ssmd1  32330  chrelat2i  32384  xrofsup  32771  prodindf  32848  ordtrest2NEWlem  33921  truae  34244  mbfmcst  34261  mbfmcnt  34270  dya2iocuni  34285  0rrv  34453  hashreprin  34635  reprgt  34636  breprexplemc  34647  breprexp  34648  circlemeth  34655  hgt750lema  34672  wevgblacfn  35114  cvmliftlem15  35303  satf0suclem  35380  fmla0disjsuc  35403  fmlasucdisj  35404  neibastop2lem  36361  tailf  36376  filnetlem4  36382  fin2so  37614  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem26  37653  poimirlem28  37655  ismblfin  37668  cnambfre  37675  itg2addnclem  37678  itg2addnc  37681  itg2gt0cn  37682  ibladdnclem  37683  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  frinfm  37742  sdclem1  37750  ssbnd  37795  rngoueqz  37947  lssatle  39016  ltrneq2  40150  tendoeq2  40776  lcmineqlem12  42041  hbtlem7  43137  trclrelexplem  43724  rfovcnvf1od  44017  dssmapf1od  44034  neik0pk1imk0  44060  collexd  44276  sswfaxreg  45004  omssaxinf2  45005  prodeq2ad  45607  0cnv  45757  itgperiod  45996  stoweidlem35  46050  stoweidlem59  46074  fourierdlem31  46153  subsaliuncllem  46372  subsaliuncl  46373  iundjiun  46475  hoiprodcl2  46570  ovn0lem  46580  hoidmvlelem3  46612  smflimlem1  46786  smflimlem2  46787  smflimlem3  46788  fundcmpsurinjlem2  47386  sprval  47466  prprval  47501  rmsupp0  48284  lincop  48325  lcoc0  48339