Theorem ralrimivw 3148

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

Syntax hints:   → wi 4   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-ral 3060

This theorem is referenced by:  r19.21v  3177  r19.37v  3179  r19.27v  3185  r19.28v  3187  2rmorex  3749  2reurex  3755  riinrab  5086  exse  5638  dmxp  5927  mpoeq12  7484  ovmpt3rabdm  7667  offveqb  7697  epweon  7764  exse2  7910  xpexgALT  7970  opabn1stprc  8046  mpoexg  8065  uniqs  8773  boxriin  8936  fisupg  9293  fisup2g  9465  fisupcl  9466  fiinfg  9496  fiinf2g  9497  ordtypelem8  9522  wemapso2  9550  cantnflem1  9686  r1val1  9783  updjud  9931  dfac12k  10144  compssiso  10371  axcclem  10454  ondomon  10560  tskuni  10780  pinq  10924  supexpr  11051  dedekind  11381  supadd  12186  supmullem2  12189  zsupss  12925  qextlt  13186  qextle  13187  xrsupsslem  13290  xrinfmsslem  13291  supxrpnf  13301  ssnn0fi  13954  recan  15287  climconst  15491  sumeq2sdv  15654  dvdsext  16268  smupvallem  16428  smumullem  16437  pc11  16817  prmreclem4  16856  vdwmc2  16916  vdwlem8  16925  vdwlem13  16930  cshwsex  17038  cshws0  17039  prdsplusg  17408  prdsmulr  17409  prdsvsca  17410  prdshom  17417  imasplusg  17467  imasmulr  17468  imasip  17471  imasaddvallem  17479  imasvscaf  17489  quslem  17493  divsfval  17497  mrcuni  17569  catideu  17623  homfeqd  17643  comfeqd  17655  2oppccomf  17675  catcoppccl  18071  catcoppcclOLD  18072  lublecllem  18317  pmtrrn  19366  pmtrfrn  19367  gsummptif1n0  19875  ip2eq  21425  frlmup4  21575  evlseu  21865  pmatcollpw2lem  22499  basdif0  22676  clsval2  22774  neif  22824  ordtbaslem  22912  ordtrest2lem  22927  lmconst  22985  cndis  23015  pnrmopn  23067  cmpfi  23132  finptfin  23242  comppfsc  23256  ptbasfi  23305  pttoponconst  23321  ptcnplem  23345  pthaus  23362  xkoptsub  23378  xkopt  23379  nrmr0reg  23473  ordthmeolem  23525  fbssfi  23561  filconn  23607  hausflim  23705  cnpflf  23725  fclscf  23749  cnpfcf  23765  alexsublem  23768  ptcmplem2  23777  ptcmplem3  23778  tsmsfbas  23852  eltsms  23857  utopbas  23960  isucn2  24004  psmetutop  24296  nrginvrcn  24429  lebnumlem3  24709  fmcfil  25020  ovolicc2lem4  25269  mbfconst  25382  i1fmul  25445  itg2const  25490  itg2cnlem2  25512  itgle  25559  ibladdlem  25569  iblabs  25578  iblabsr  25579  iblmulc2  25580  bddmulibl  25588  bddiblnc  25591  ellimc2  25626  limcnlp  25627  c1lip1  25749  itgpowd  25802  ply1nzb  25875  ulm0  26139  itgulm2  26157  dchrhash  27010  lgsquadlem2  27120  2sqlem10  27167  dchrisum  27231  rpvmasum2  27251  pntlemj  27342  bday0b  27568  axcontlem12  28500  nbgr0edg  28881  rusgr1vtx  29112  uspgr2wlkeq2  29171  clwwlknondisj  29631  ip2eqi  30376  ubthlem1  30390  hial2eq  30626  pjnmopi  31668  ssmd1  31831  chrelat2i  31885  xrofsup  32247  ordtrest2NEWlem  33200  prodindf  33319  truae  33539  mbfmcst  33556  mbfmcnt  33565  dya2iocuni  33580  0rrv  33748  hashreprin  33930  reprgt  33931  breprexplemc  33942  breprexp  33943  circlemeth  33950  hgt750lema  33967  cvmliftlem15  34587  satf0suclem  34664  fmla0disjsuc  34687  fmlasucdisj  34688  neibastop2lem  35548  tailf  35563  filnetlem4  35569  fin2so  36778  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem26  36817  poimirlem28  36819  ismblfin  36832  cnambfre  36839  itg2addnclem  36842  itg2addnc  36845  itg2gt0cn  36846  ibladdnclem  36847  iblabsnc  36855  iblmulc2nc  36856  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  frinfm  36906  sdclem1  36914  ssbnd  36959  rngoueqz  37111  lssatle  38188  ltrneq2  39322  tendoeq2  39948  lcmineqlem12  41211  hbtlem7  42169  trclrelexplem  42764  rfovcnvf1od  43057  dssmapf1od  43074  neik0pk1imk0  43100  collexd  43318  prodeq2ad  44606  0cnv  44756  itgperiod  44995  stoweidlem35  45049  stoweidlem59  45073  fourierdlem31  45152  subsaliuncllem  45371  subsaliuncl  45372  iundjiun  45474  hoiprodcl2  45569  ovn0lem  45579  hoidmvlelem3  45611  smflimlem1  45785  smflimlem2  45786  smflimlem3  45787  fundcmpsurinjlem2  46365  sprval  46445  prprval  46480  rmsupp0  47132  lincop  47176  lcoc0  47190