Theorem ralrimivw 3160

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 3155	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  r19.21v  3189  r19.37v  3190  r19.27v  3193  r19.28v  3195  2rmorex  3715  2reurex  3721  riinrab  5048  exse  5619  mpoeq12  7489  ovmpt3rabdm  7676  offveqb  7708  epweon  7777  exse2  7917  xpexgALT  7981  opabn1stprc  8058  mpoexg  8078  boxriin  8950  fisupg  9261  fisup2g  9442  fisupcl  9443  fiinfg  9474  fiinf2g  9475  ordtypelem8  9500  wemapso2  9528  cantnflem1  9671  r1val1  9771  updjud  9942  dfac12k  10153  compssiso  10379  axcclem  10462  ondomon  10574  tskuni  10795  pinq  10939  supexpr  11066  dedekind  11400  supadd  12210  supmullem2  12213  zsupss  12989  qextlt  13257  qextle  13258  xrsupsslem  13361  xrinfmsslem  13362  supxrpnf  13372  ssnn0fi  14051  recan  15426  climconst  15632  dvdsext  16415  smupvallem  16577  smumullem  16586  pc11  16976  prmreclem4  17015  vdwmc2  17075  vdwlem8  17084  vdwlem13  17089  cshwsex  17196  cshws0  17197  prdsplusg  17547  prdsmulr  17548  prdsvsca  17549  prdshom  17556  imasplusg  17607  imasmulr  17608  imasip  17611  imasaddvallem  17619  imasvscaf  17629  quslem  17633  divsfval  17637  mrcuni  17713  catideu  17767  homfeqd  17787  comfeqd  17799  2oppccomf  17817  catcoppccl  18210  lublecllem  18450  chnfi  18726  pmtrrn  19585  pmtrfrn  19586  gsummptif1n0  20094  ip2eq  21867  frlmup4  22015  evlseu  22300  matunitlindflem1  22902  matunitlindflem2  22903  pmatcollpw2lem  23003  basdif0  23179  clsval2  23276  neif  23326  ordtbaslem  23414  ordtrest2lem  23429  lmconst  23487  cndis  23517  pnrmopn  23569  cmpfi  23634  finptfin  23745  comppfsc  23759  ptbasfi  23808  pttoponconst  23824  ptcnplem  23848  pthaus  23865  xkoptsub  23881  xkopt  23882  nrmr0reg  23976  ordthmeolem  24028  fbssfi  24064  filconn  24110  hausflim  24208  cnpflf  24228  fclscf  24252  cnpfcf  24268  alexsublem  24271  ptcmplem2  24280  ptcmplem3  24281  tsmsfbas  24355  eltsms  24360  utopbas  24462  isucn2  24505  psmetutop  24794  nrginvrcn  24919  lebnumlem3  25192  fmcfil  25501  ovolicc2lem4  25749  mbfconst  25862  i1fmul  25925  itg2const  25969  itg2cnlem2  25991  itgle  26039  ibladdlem  26049  iblabs  26058  iblabsr  26059  iblmulc2  26060  bddmulibl  26068  bddiblnc  26071  ellimc2  26106  limcnlp  26107  c1lip1  26226  itgpowd  26279  ply1nzb  26350  ulm0  26624  itgulm2  26642  dchrhash  27505  lgsquadlem2  27615  2sqlem10  27662  dchrisum  27726  rpvmasum2  27746  pntlemj  27837  bday0b  28076  axcontlem12  29418  nbgr0edg  29803  rusgr1vtx  30034  uspgr2wlkeq2  30092  clwwlknondisj  30567  ip2eqi  31323  ubthlem1  31337  hial2eq  31573  pjnmopi  32615  ssmd1  32778  chrelat2i  32832  xrofsup  33225  prodindf  33295  selvply1rhmlemb  34016  extdgfialglem2  34190  ordtrest2NEWlem  34419  truae  34741  mbfmcst  34757  mbfmcnt  34766  dya2iocuni  34781  0rrv  34949  hashreprin  35115  reprgt  35116  breprexplemc  35127  breprexp  35128  circlemeth  35135  hgt750lema  35152  fineqvnttrclselem1  35634  fineqvnttrclse  35637  vonf1wev  35692  vonf1owevOLD  35694  wevgblacfn  35695  onvfowev  35700  cvmliftlem15  35864  satf0suclem  35941  fmla0disjsuc  35964  fmlasucdisj  35965  neibastop2lem  36966  tailf  36981  filnetlem4  36987  fin2so  38348  poimirlem26  38382  poimirlem28  38384  ismblfin  38397  cnambfre  38404  itg2addnclem  38407  itg2addnc  38410  itg2gt0cn  38411  ibladdnclem  38412  iblabsnc  38420  iblmulc2nc  38421  ftc1anclem6  38434  ftc1anclem7  38435  ftc1anclem8  38436  ftc1anc  38437  frinfm  38472  sdclem1  38480  ssbnd  38525  rngoueqz  38677  lssatle  39875  ltrneq2  41008  tendoeq2  41634  lcmineqlem12  42893  hbtlem7  43953  trclrelexplem  44538  rfovcnvf1od  44831  dssmapf1od  44848  neik0pk1imk0  44874  collexd  45068  sswfaxreg  45797  omssaxinf2  45798  prodeq2ad  46409  0cnv  46557  itgperiod  46796  stoweidlem35  46850  stoweidlem59  46874  fourierdlem31  46953  subsaliuncllem  47172  subsaliuncl  47173  iundjiun  47275  hoiprodcl2  47370  ovn0lem  47380  hoidmvlelem3  47412  smflimlem1  47586  smflimlem2  47587  smflimlem3  47588  tmachlem-tpbase  47754  tmachlem-extpcover  47760  tmachlem-agreefin  47763  fundcmpsurinjlem2  48286  sprval  48366  prprval  48401  rmsupp0  49285  lincop  49325  lcoc0  49339  nelsubclem  49980