Theorem ralrimivw 3130

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3045

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 3046

This theorem is referenced by:  r19.21v  3159  r19.37v  3161  r19.27v  3167  r19.28v  3169  2rmorex  3728  2reurex  3734  riinrab  5051  exse  5601  dmxpOLD  5896  mpoeq12  7465  ovmpt3rabdm  7651  offveqb  7683  epweon  7754  exse2  7896  xpexgALT  7963  opabn1stprc  8040  mpoexg  8058  boxriin  8916  fisupg  9242  fisup2g  9427  fisupcl  9428  fiinfg  9459  fiinf2g  9460  ordtypelem8  9485  wemapso2  9513  cantnflem1  9649  r1val1  9746  updjud  9894  dfac12k  10108  compssiso  10334  axcclem  10417  ondomon  10523  tskuni  10743  pinq  10887  supexpr  11014  dedekind  11344  supadd  12158  supmullem2  12161  zsupss  12903  qextlt  13170  qextle  13171  xrsupsslem  13274  xrinfmsslem  13275  supxrpnf  13285  ssnn0fi  13957  recan  15310  climconst  15516  sumeq2sdvOLD  15677  dvdsext  16298  smupvallem  16460  smumullem  16469  pc11  16858  prmreclem4  16897  vdwmc2  16957  vdwlem8  16966  vdwlem13  16971  cshwsex  17078  cshws0  17079  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  imasplusg  17487  imasmulr  17488  imasip  17491  imasaddvallem  17499  imasvscaf  17509  quslem  17513  divsfval  17517  mrcuni  17589  catideu  17643  homfeqd  17663  comfeqd  17675  2oppccomf  17693  catcoppccl  18086  lublecllem  18326  pmtrrn  19394  pmtrfrn  19395  gsummptif1n0  19903  ip2eq  21569  frlmup4  21717  evlseu  21997  pmatcollpw2lem  22671  basdif0  22847  clsval2  22944  neif  22994  ordtbaslem  23082  ordtrest2lem  23097  lmconst  23155  cndis  23185  pnrmopn  23237  cmpfi  23302  finptfin  23412  comppfsc  23426  ptbasfi  23475  pttoponconst  23491  ptcnplem  23515  pthaus  23532  xkoptsub  23548  xkopt  23549  nrmr0reg  23643  ordthmeolem  23695  fbssfi  23731  filconn  23777  hausflim  23875  cnpflf  23895  fclscf  23919  cnpfcf  23935  alexsublem  23938  ptcmplem2  23947  ptcmplem3  23948  tsmsfbas  24022  eltsms  24027  utopbas  24130  isucn2  24173  psmetutop  24462  nrginvrcn  24587  lebnumlem3  24869  fmcfil  25179  ovolicc2lem4  25428  mbfconst  25541  i1fmul  25604  itg2const  25648  itg2cnlem2  25670  itgle  25718  ibladdlem  25728  iblabs  25737  iblabsr  25738  iblmulc2  25739  bddmulibl  25747  bddiblnc  25750  ellimc2  25785  limcnlp  25786  c1lip1  25909  itgpowd  25964  ply1nzb  26035  ulm0  26307  itgulm2  26325  dchrhash  27189  lgsquadlem2  27299  2sqlem10  27346  dchrisum  27410  rpvmasum2  27430  pntlemj  27521  bday0b  27749  axcontlem12  28909  nbgr0edg  29291  rusgr1vtx  29523  uspgr2wlkeq2  29582  clwwlknondisj  30047  ip2eqi  30792  ubthlem1  30806  hial2eq  31042  pjnmopi  32084  ssmd1  32247  chrelat2i  32301  xrofsup  32697  prodindf  32793  ordtrest2NEWlem  33919  truae  34240  mbfmcst  34257  mbfmcnt  34266  dya2iocuni  34281  0rrv  34449  hashreprin  34618  reprgt  34619  breprexplemc  34630  breprexp  34631  circlemeth  34638  hgt750lema  34655  vonf1owev  35102  wevgblacfn  35103  cvmliftlem15  35292  satf0suclem  35369  fmla0disjsuc  35392  fmlasucdisj  35393  neibastop2lem  36355  tailf  36370  filnetlem4  36376  fin2so  37608  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem26  37647  poimirlem28  37649  ismblfin  37662  cnambfre  37669  itg2addnclem  37672  itg2addnc  37675  itg2gt0cn  37676  ibladdnclem  37677  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  frinfm  37736  sdclem1  37744  ssbnd  37789  rngoueqz  37941  lssatle  39015  ltrneq2  40149  tendoeq2  40775  lcmineqlem12  42035  hbtlem7  43121  trclrelexplem  43707  rfovcnvf1od  44000  dssmapf1od  44017  neik0pk1imk0  44043  collexd  44253  sswfaxreg  44984  omssaxinf2  44985  prodeq2ad  45597  0cnv  45747  itgperiod  45986  stoweidlem35  46040  stoweidlem59  46064  fourierdlem31  46143  subsaliuncllem  46362  subsaliuncl  46363  iundjiun  46465  hoiprodcl2  46560  ovn0lem  46570  hoidmvlelem3  46602  smflimlem1  46776  smflimlem2  46777  smflimlem3  46778  fundcmpsurinjlem2  47404  sprval  47484  prprval  47519  rmsupp0  48360  lincop  48401  lcoc0  48415  nelsubclem  49060