Theorem ralrimivw 2950

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  2rmorex  3379  riinrab  4532  exse  5002  dmxp  5265  mpt2eq12  6613  ovmpt3rabdm  6790  offveqb  6817  exse2  6998  xpexgALT  7052  mpt2exg  7134  uniqs  7694  boxriin  7836  fisupg  8093  fisup2g  8257  fisupcl  8258  fiinfg  8288  fiinf2g  8289  ordtypelem8  8313  wemapso2  8341  cantnflem1  8469  r1val1  8532  scottex  8631  dfac12k  8852  compssiso  9079  axcclem  9162  ondomon  9264  tskuni  9484  pinq  9628  supexpr  9755  dedekind  10079  supadd  10868  supmullem2  10871  zsupss  11653  qextlt  11908  qextle  11909  xrsupsslem  12009  xrinfmsslem  12010  supxrpnf  12020  ssnn0fi  12646  recan  13924  climconst  14122  dvdsext  14881  smupvallem  15043  smumullem  15052  pc11  15422  prmreclem4  15461  vdwmc2  15521  vdwlem8  15530  vdwlem13  15535  cshwsex  15645  cshws0  15646  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  imasplusg  16000  imasmulr  16001  imasip  16004  imasaddvallem  16012  imasvscaf  16022  quslem  16026  divsfval  16030  mrcuni  16104  catideu  16159  homfeqd  16178  comfeqd  16190  2oppccomf  16208  catcoppccl  16581  lublecllem  16811  pmtrrn  17700  pmtrfrn  17701  gsummptif1n0  18188  evlseu  19337  ip2eq  19817  frlmup4  19959  pmatcollpw2lem  20401  basdif0  20568  clsval2  20664  neif  20714  ordtbaslem  20802  ordtrest2lem  20817  lmconst  20875  cndis  20905  pnrmopn  20957  cmpfi  21021  finptfin  21131  comppfsc  21145  ptbasfi  21194  pttoponconst  21210  ptcnplem  21234  pthaus  21251  xkoptsub  21267  xkopt  21268  nrmr0reg  21362  ordthmeolem  21414  fbssfi  21451  filcon  21497  hausflim  21595  cnpflf  21615  fclscf  21639  cnpfcf  21655  alexsublem  21658  ptcmplem2  21667  ptcmplem3  21668  tsmsfbas  21741  eltsms  21746  utopbas  21849  isucn2  21893  psmetutop  22182  nrginvrcn  22306  lebnumlem3  22570  fmcfil  22878  ovolicc2lem4  23095  mbfconst  23208  i1fmul  23269  itg2const  23313  itg2cnlem2  23335  itgle  23382  ibladdlem  23392  iblabs  23401  iblabsr  23402  iblmulc2  23403  bddmulibl  23411  ellimc2  23447  limcnlp  23448  c1lip1  23564  ply1nzb  23686  ulm0  23949  itgulm2  23967  dchrhash  24796  lgsquadlem2  24906  2sqlem10  24953  dchrisum  24981  rpvmasum2  25001  pntlemj  25092  axcontlem12  25655  uvtxnb  26025  usg2wlkeq2  26237  numclwwlkdisj  26607  ip2eqi  27096  ubthlem1  27110  hial2eq  27347  occon  27530  spanss  27591  pjnmopi  28391  ssmd1  28554  chrelat2i  28608  xrofsup  28923  ordtrest2NEWlem  29296  truae  29633  mbfmcst  29648  mbfmcnt  29657  dya2iocuni  29672  0rrv  29840  cvmliftlem15  30534  trpredss  30973  neibastop2lem  31525  tailf  31540  filnetlem4  31546  fin2so  32566  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem26  32605  poimirlem28  32607  ismblfin  32620  cnambfre  32628  itg2addnclem  32631  itg2addnc  32634  itg2gt0cn  32635  ibladdnclem  32636  iblabsnc  32644  iblmulc2nc  32645  bddiblnc  32650  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  frinfm  32700  sdclem1  32709  ssbnd  32757  rngoueqz  32909  lssatle  33320  ltrneq2  34452  tendoeq2  35080  hbtlem7  36714  itgoss  36752  itgpowd  36819  trclrelexplem  37022  rfovcnvf1od  37318  dssmapf1od  37335  sumeq2ad  38632  prodeq2ad  38659  itgperiod  38873  stoweidlem35  38928  stoweidlem59  38952  fourierdlem31  39031  subsaliuncllem  39251  subsaliuncl  39252  iundjiun  39353  hoiprodcl2  39445  ovnsslelem  39450  ovn0lem  39455  hoidmvlelem3  39487  smflimlem1  39657  smflimlem2  39658  smflimlem3  39659  2reurex  39830  opabn1stprc  40318  nbgr0edg  40579  rusgr1vtx  40788  uspgr2wlkeq2  40855  clwwlksndisj  41280  frgrhash2wsp  41497  rmsupp0  41943  lincop  41991  lcoc0  42005