Theorem ralrimivw 3131

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ral 3051

This theorem is referenced by:  r19.21v  3160  r19.37v  3161  r19.27v  3164  r19.28v  3166  2rmorex  3711  2reurex  3717  riinrab  5038  exse  5583  mpoeq12  7431  ovmpt3rabdm  7617  offveqb  7649  epweon  7720  exse2  7859  xpexgALT  7925  opabn1stprc  8002  mpoexg  8020  boxriin  8880  fisupg  9190  fisup2g  9374  fisupcl  9375  fiinfg  9406  fiinf2g  9407  ordtypelem8  9432  wemapso2  9460  cantnflem1  9600  r1val1  9700  updjud  9848  dfac12k  10060  compssiso  10286  axcclem  10369  ondomon  10475  tskuni  10696  pinq  10840  supexpr  10967  dedekind  11298  supadd  12112  supmullem2  12115  zsupss  12852  qextlt  13120  qextle  13121  xrsupsslem  13224  xrinfmsslem  13225  supxrpnf  13235  ssnn0fi  13910  recan  15262  climconst  15468  sumeq2sdvOLD  15629  dvdsext  16250  smupvallem  16412  smumullem  16421  pc11  16810  prmreclem4  16849  vdwmc2  16909  vdwlem8  16918  vdwlem13  16923  cshwsex  17030  cshws0  17031  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdshom  17389  imasplusg  17440  imasmulr  17441  imasip  17444  imasaddvallem  17452  imasvscaf  17462  quslem  17466  divsfval  17470  mrcuni  17546  catideu  17600  homfeqd  17620  comfeqd  17632  2oppccomf  17650  catcoppccl  18043  lublecllem  18283  chnfi  18559  pmtrrn  19388  pmtrfrn  19389  gsummptif1n0  19897  ip2eq  21610  frlmup4  21758  evlseu  22040  pmatcollpw2lem  22723  basdif0  22899  clsval2  22996  neif  23046  ordtbaslem  23134  ordtrest2lem  23149  lmconst  23207  cndis  23237  pnrmopn  23289  cmpfi  23354  finptfin  23464  comppfsc  23478  ptbasfi  23527  pttoponconst  23543  ptcnplem  23567  pthaus  23584  xkoptsub  23600  xkopt  23601  nrmr0reg  23695  ordthmeolem  23747  fbssfi  23783  filconn  23829  hausflim  23927  cnpflf  23947  fclscf  23971  cnpfcf  23987  alexsublem  23990  ptcmplem2  23999  ptcmplem3  24000  tsmsfbas  24074  eltsms  24079  utopbas  24181  isucn2  24224  psmetutop  24513  nrginvrcn  24638  lebnumlem3  24920  fmcfil  25230  ovolicc2lem4  25479  mbfconst  25592  i1fmul  25655  itg2const  25699  itg2cnlem2  25721  itgle  25769  ibladdlem  25779  iblabs  25788  iblabsr  25789  iblmulc2  25790  bddmulibl  25798  bddiblnc  25801  ellimc2  25836  limcnlp  25837  c1lip1  25960  itgpowd  26015  ply1nzb  26086  ulm0  26358  itgulm2  26376  dchrhash  27240  lgsquadlem2  27350  2sqlem10  27397  dchrisum  27461  rpvmasum2  27481  pntlemj  27572  bday0b  27809  axcontlem12  29029  nbgr0edg  29411  rusgr1vtx  29643  uspgr2wlkeq2  29701  clwwlknondisj  30167  ip2eqi  30912  ubthlem1  30926  hial2eq  31162  pjnmopi  32204  ssmd1  32367  chrelat2i  32421  xrofsup  32826  prodindf  32923  extdgfialglem2  33829  ordtrest2NEWlem  34058  truae  34379  mbfmcst  34395  mbfmcnt  34404  dya2iocuni  34419  0rrv  34587  hashreprin  34756  reprgt  34757  breprexplemc  34768  breprexp  34769  circlemeth  34776  hgt750lema  34793  fineqvnttrclselem1  35256  fineqvnttrclse  35259  vonf1owev  35281  wevgblacfn  35282  cvmliftlem15  35471  satf0suclem  35548  fmla0disjsuc  35571  fmlasucdisj  35572  neibastop2lem  36533  tailf  36548  filnetlem4  36554  fin2so  37777  matunitlindflem1  37786  matunitlindflem2  37787  poimirlem26  37816  poimirlem28  37818  ismblfin  37831  cnambfre  37838  itg2addnclem  37841  itg2addnc  37844  itg2gt0cn  37845  ibladdnclem  37846  iblabsnc  37854  iblmulc2nc  37855  ftc1anclem6  37868  ftc1anclem7  37869  ftc1anclem8  37870  ftc1anc  37871  frinfm  37905  sdclem1  37913  ssbnd  37958  rngoueqz  38110  lssatle  39310  ltrneq2  40443  tendoeq2  41069  lcmineqlem12  42329  hbtlem7  43404  trclrelexplem  43989  rfovcnvf1od  44282  dssmapf1od  44299  neik0pk1imk0  44325  collexd  44535  sswfaxreg  45265  omssaxinf2  45266  prodeq2ad  45875  0cnv  46023  itgperiod  46262  stoweidlem35  46316  stoweidlem59  46340  fourierdlem31  46419  subsaliuncllem  46638  subsaliuncl  46639  iundjiun  46741  hoiprodcl2  46836  ovn0lem  46846  hoidmvlelem3  46878  smflimlem1  47052  smflimlem2  47053  smflimlem3  47054  fundcmpsurinjlem2  47682  sprval  47762  prprval  47797  rmsupp0  48651  lincop  48691  lcoc0  48705  nelsubclem  49349