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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106

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 1911

This theorem depends on definitions:  df-bi 210  df-ral 3111

This theorem is referenced by:  r19.27v  3151  r19.28v  3152  r19.37v  3298  2rmorex  3693  2reurex  3698  riinrab  4969  exse  5483  dmxp  5763  mpoeq12  7206  ovmpt3rabdm  7384  offveqb  7411  exse2  7604  xpexgALT  7664  opabn1stprc  7738  mpoexg  7757  uniqs  8340  boxriin  8487  fisupg  8750  fisup2g  8916  fisupcl  8917  fiinfg  8947  fiinf2g  8948  ordtypelem8  8973  wemapso2  9001  cantnflem1  9136  r1val1  9199  scottex  9298  updjud  9347  dfac12k  9558  compssiso  9785  axcclem  9868  ondomon  9974  tskuni  10194  pinq  10338  supexpr  10465  dedekind  10792  supadd  11596  supmullem2  11599  zsupss  12325  qextlt  12584  qextle  12585  xrsupsslem  12688  xrinfmsslem  12689  supxrpnf  12699  ssnn0fi  13348  recan  14688  climconst  14892  sumeq2sdv  15053  dvdsext  15663  smupvallem  15822  smumullem  15831  pc11  16206  prmreclem4  16245  vdwmc2  16305  vdwlem8  16314  vdwlem13  16319  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  19079  ip2eq  20342  frlmup4  20490  evlseu  20755  pmatcollpw2lem  21382  basdif0  21558  clsval2  21655  neif  21705  ordtbaslem  21793  ordtrest2lem  21808  lmconst  21866  cndis  21896  pnrmopn  21948  cmpfi  22013  finptfin  22123  comppfsc  22137  ptbasfi  22186  pttoponconst  22202  ptcnplem  22226  pthaus  22243  xkoptsub  22259  xkopt  22260  nrmr0reg  22354  ordthmeolem  22406  fbssfi  22442  filconn  22488  hausflim  22586  cnpflf  22606  fclscf  22630  cnpfcf  22646  alexsublem  22649  ptcmplem2  22658  ptcmplem3  22659  tsmsfbas  22733  eltsms  22738  utopbas  22841  isucn2  22885  psmetutop  23174  nrginvrcn  23298  lebnumlem3  23568  fmcfil  23876  ovolicc2lem4  24124  mbfconst  24237  i1fmul  24300  itg2const  24344  itg2cnlem2  24366  itgle  24413  ibladdlem  24423  iblabs  24432  iblabsr  24433  iblmulc2  24434  bddmulibl  24442  bddiblnc  24445  ellimc2  24480  limcnlp  24481  c1lip1  24600  itgpowd  24653  ply1nzb  24723  ulm0  24986  itgulm2  25004  dchrhash  25855  lgsquadlem2  25965  2sqlem10  26012  dchrisum  26076  rpvmasum2  26096  pntlemj  26187  axcontlem12  26769  nbgr0edg  27147  rusgr1vtx  27378  uspgr2wlkeq2  27436  clwwlknondisj  27896  ip2eqi  28639  ubthlem1  28653  hial2eq  28889  occon  29070  spanss  29131  pjnmopi  29931  ssmd1  30094  chrelat2i  30148  xrofsup  30518  ordtrest2NEWlem  31275  prodindf  31392  truae  31612  mbfmcst  31627  mbfmcnt  31636  dya2iocuni  31651  0rrv  31819  hashreprin  32001  reprgt  32002  breprexplemc  32013  breprexp  32014  circlemeth  32021  hgt750lema  32038  cvmliftlem15  32658  satf0suclem  32735  fmla0disjsuc  32758  fmlasucdisj  32759  trpredss  33181  neibastop2lem  33821  tailf  33836  filnetlem4  33842  fin2so  35044  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem26  35083  poimirlem28  35085  ismblfin  35098  cnambfre  35105  itg2addnclem  35108  itg2addnc  35111  itg2gt0cn  35112  ibladdnclem  35113  iblabsnc  35121  iblmulc2nc  35122  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  frinfm  35173  sdclem1  35181  ssbnd  35226  rngoueqz  35378  lssatle  36311  ltrneq2  37444  tendoeq2  38070  lcmineqlem12  39328  hbtlem7  40069  itgoss  40107  trclrelexplem  40412  rfovcnvf1od  40705  dssmapf1od  40722  neik0pk1imk0  40750  collexd  40965  prodeq2ad  42234  0cnv  42384  itgperiod  42623  stoweidlem35  42677  stoweidlem59  42701  fourierdlem31  42780  subsaliuncllem  42997  subsaliuncl  42998  iundjiun  43099  hoiprodcl2  43194  ovnsslelem  43199  ovn0lem  43204  hoidmvlelem3  43236  smflimlem1  43404  smflimlem2  43405  smflimlem3  43406  fundcmpsurinjlem2  43916  sprval  43996  prprval  44031  rmsupp0  44770  lincop  44817  lcoc0  44831