Theorem ralrimivw 3158

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

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

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 3077

This theorem is used by:  r19.21v  3187  r19.37v  3188  r19.27v  3191  r19.28v  3193  2rmorex  3712  2reurex  3718  riinrab  5044  exse  5608  mpoeq12  7482  ovmpt3rabdm  7669  offveqb  7704  epweon  7773  exse2  7913  xpexgALT  7977  opabn1stprc  8053  mpoexg  8073  boxriin  8947  fisupg  9258  fisup2g  9439  fisupcl  9440  fiinfg  9471  fiinf2g  9472  ordtypelem8  9497  wemapso2  9525  cantnflem1  9668  r1val1  9768  updjud  9972  dfac12k  10183  compssiso  10409  axcclem  10492  ondomon  10604  tskuni  10825  pinq  10969  supexpr  11096  dedekind  11430  supadd  12240  supmullem2  12243  zsupss  13019  qextlt  13288  qextle  13289  xrsupsslem  13392  xrinfmsslem  13393  supxrpnf  13403  ssnn0fi  14082  recan  15457  climconst  15663  dvdsext  16444  smupvallem  16606  smumullem  16615  pc11  17005  prmreclem4  17044  vdwmc2  17104  vdwlem8  17113  vdwlem13  17118  cshwsex  17225  cshws0  17226  prdsplusg  17576  prdsmulr  17577  prdsvsca  17578  prdshom  17585  imasplusg  17636  imasmulr  17637  imasip  17640  imasaddvallem  17648  imasvscaf  17658  quslem  17662  divsfval  17666  mrcuni  17742  catideu  17796  homfeqd  17816  comfeqd  17828  2oppccomf  17846  catcoppccl  18239  lublecllem  18479  chnfi  18755  pmtrrn  19618  pmtrfrn  19619  gsummptif1n0  20127  ip2eq  21906  frlmup4  22054  evlseu  22339  matunitlindflem1  22941  matunitlindflem2  22942  pmatcollpw2lem  23042  basdif0  23218  clsval2  23315  neif  23365  ordtbaslem  23453  ordtrest2lem  23468  lmconst  23526  cndis  23556  pnrmopn  23608  cmpfi  23673  finptfin  23784  comppfsc  23798  ptbasfi  23847  pttoponconst  23863  ptcnplem  23887  pthaus  23904  xkoptsub  23920  xkopt  23921  nrmr0reg  24015  ordthmeolem  24067  fbssfi  24103  filconn  24149  hausflim  24247  cnpflf  24267  fclscf  24291  cnpfcf  24307  alexsublem  24310  ptcmplem2  24319  ptcmplem3  24320  tsmsfbas  24394  eltsms  24399  utopbas  24501  isucn2  24544  psmetutop  24833  nrginvrcn  24958  lebnumlem3  25231  fmcfil  25540  ovolicc2lem4  25788  mbfconst  25901  i1fmul  25964  itg2const  26008  itg2cnlem2  26030  itgle  26077  ibladdlem  26087  iblabs  26096  iblabsr  26097  iblmulc2  26098  bddmulibl  26106  bddiblnc  26109  ellimc2  26144  limcnlp  26145  c1lip1  26264  itgpowd  26317  ply1nzb  26388  ulm0  26667  itgulm2  26685  dchrhash  27547  lgsquadlem2  27657  2sqlem10  27704  dchrisum  27768  rpvmasum2  27788  pntlemj  27879  bday0b  28118  axcontlem12  29472  nbgr0edg  29857  rusgr1vtx  30088  uspgr2wlkeq2  30146  clwwlknondisj  30621  ip2eqi  31377  ubthlem1  31391  hial2eq  31627  pjnmopi  32669  ssmd1  32832  chrelat2i  32886  xrofsup  33278  prodindf  33348  selvply1rhmlemb  34070  extdgfialglem2  34244  ordtrest2NEWlem  34473  truae  34795  mbfmcst  34811  mbfmcnt  34820  dya2iocuni  34835  0rrv  35003  hashreprin  35169  reprgt  35170  breprexplemc  35181  breprexp  35182  circlemeth  35189  hgt750lema  35206  fineqvnttrclselem1  35708  fineqvnttrclse  35711  vonf1wev  35806  vonf1owevOLD  35808  wevgblacfn  35809  onvfowev  35814  cvmliftlem15  35978  satf0suclem  36055  fmla0disjsuc  36078  fmlasucdisj  36079  neibastop2lem  37064  tailf  37079  filnetlem4  37085  fin2so  38444  poimirlem26  38478  poimirlem28  38480  ismblfin  38493  cnambfre  38500  itg2addnclem  38503  itg2addnc  38506  itg2gt0cn  38507  ibladdnclem  38508  iblabsnc  38516  iblmulc2nc  38517  ftc1anclem6  38530  ftc1anclem7  38531  ftc1anclem8  38532  ftc1anc  38533  frinfm  38583  sdclem1  38591  ssbnd  38636  rngoueqz  38788  lssatle  39986  ltrneq2  41119  tendoeq2  41745  lcmineqlem12  43004  hbtlem7  44064  trclrelexplem  44649  rfovcnvf1od  44942  dssmapf1od  44959  neik0pk1imk0  44985  collexd  45179  sswfaxreg  45908  omssaxinf2  45909  prodeq2ad  46520  0cnv  46668  itgperiod  46907  stoweidlem35  46961  stoweidlem59  46985  fourierdlem31  47064  subsaliuncllem  47283  subsaliuncl  47284  iundjiun  47386  hoiprodcl2  47481  ovn0lem  47491  hoidmvlelem3  47523  smflimlem1  47697  smflimlem2  47698  smflimlem3  47699  tmachlem-tpbase  47865  tmachlem-extpcover  47871  tmachlem-agreefin  47874  fundcmpsurinjlem2  48397  sprval  48477  prprval  48512  rmsupp0  49396  lincop  49436  lcoc0  49450  nelsubclem  50091