Theorem ralrimivw 3133

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

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

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 3053

This theorem is referenced by:  r19.21v  3162  r19.37v  3163  r19.27v  3166  r19.28v  3168  2rmorex  3713  2reurex  3719  riinrab  5040  exse  5585  mpoeq12  7433  ovmpt3rabdm  7619  offveqb  7651  epweon  7722  exse2  7861  xpexgALT  7927  opabn1stprc  8004  mpoexg  8022  boxriin  8882  fisupg  9192  fisup2g  9376  fisupcl  9377  fiinfg  9408  fiinf2g  9409  ordtypelem8  9434  wemapso2  9462  cantnflem1  9602  r1val1  9702  updjud  9850  dfac12k  10062  compssiso  10288  axcclem  10371  ondomon  10477  tskuni  10698  pinq  10842  supexpr  10969  dedekind  11300  supadd  12114  supmullem2  12117  zsupss  12854  qextlt  13122  qextle  13123  xrsupsslem  13226  xrinfmsslem  13227  supxrpnf  13237  ssnn0fi  13912  recan  15264  climconst  15470  sumeq2sdvOLD  15631  dvdsext  16252  smupvallem  16414  smumullem  16423  pc11  16812  prmreclem4  16851  vdwmc2  16911  vdwlem8  16920  vdwlem13  16925  cshwsex  17032  cshws0  17033  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  prdshom  17391  imasplusg  17442  imasmulr  17443  imasip  17446  imasaddvallem  17454  imasvscaf  17464  quslem  17468  divsfval  17472  mrcuni  17548  catideu  17602  homfeqd  17622  comfeqd  17634  2oppccomf  17652  catcoppccl  18045  lublecllem  18285  chnfi  18561  pmtrrn  19390  pmtrfrn  19391  gsummptif1n0  19899  ip2eq  21612  frlmup4  21760  evlseu  22042  pmatcollpw2lem  22725  basdif0  22901  clsval2  22998  neif  23048  ordtbaslem  23136  ordtrest2lem  23151  lmconst  23209  cndis  23239  pnrmopn  23291  cmpfi  23356  finptfin  23466  comppfsc  23480  ptbasfi  23529  pttoponconst  23545  ptcnplem  23569  pthaus  23586  xkoptsub  23602  xkopt  23603  nrmr0reg  23697  ordthmeolem  23749  fbssfi  23785  filconn  23831  hausflim  23929  cnpflf  23949  fclscf  23973  cnpfcf  23989  alexsublem  23992  ptcmplem2  24001  ptcmplem3  24002  tsmsfbas  24076  eltsms  24081  utopbas  24183  isucn2  24226  psmetutop  24515  nrginvrcn  24640  lebnumlem3  24922  fmcfil  25232  ovolicc2lem4  25481  mbfconst  25594  i1fmul  25657  itg2const  25701  itg2cnlem2  25723  itgle  25771  ibladdlem  25781  iblabs  25790  iblabsr  25791  iblmulc2  25792  bddmulibl  25800  bddiblnc  25803  ellimc2  25838  limcnlp  25839  c1lip1  25962  itgpowd  26017  ply1nzb  26088  ulm0  26360  itgulm2  26378  dchrhash  27242  lgsquadlem2  27352  2sqlem10  27399  dchrisum  27463  rpvmasum2  27483  pntlemj  27574  bday0b  27813  axcontlem12  29052  nbgr0edg  29434  rusgr1vtx  29666  uspgr2wlkeq2  29724  clwwlknondisj  30190  ip2eqi  30935  ubthlem1  30949  hial2eq  31185  pjnmopi  32227  ssmd1  32390  chrelat2i  32444  xrofsup  32849  prodindf  32946  extdgfialglem2  33852  ordtrest2NEWlem  34081  truae  34402  mbfmcst  34418  mbfmcnt  34427  dya2iocuni  34442  0rrv  34610  hashreprin  34779  reprgt  34780  breprexplemc  34791  breprexp  34792  circlemeth  34799  hgt750lema  34816  fineqvnttrclselem1  35279  fineqvnttrclse  35282  vonf1owev  35304  wevgblacfn  35305  cvmliftlem15  35494  satf0suclem  35571  fmla0disjsuc  35594  fmlasucdisj  35595  neibastop2lem  36556  tailf  36571  filnetlem4  36577  fin2so  37810  matunitlindflem1  37819  matunitlindflem2  37820  poimirlem26  37849  poimirlem28  37851  ismblfin  37864  cnambfre  37871  itg2addnclem  37874  itg2addnc  37877  itg2gt0cn  37878  ibladdnclem  37879  iblabsnc  37887  iblmulc2nc  37888  ftc1anclem6  37901  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  frinfm  37938  sdclem1  37946  ssbnd  37991  rngoueqz  38143  lssatle  39343  ltrneq2  40476  tendoeq2  41102  lcmineqlem12  42362  hbtlem7  43434  trclrelexplem  44019  rfovcnvf1od  44312  dssmapf1od  44329  neik0pk1imk0  44355  collexd  44565  sswfaxreg  45295  omssaxinf2  45296  prodeq2ad  45905  0cnv  46053  itgperiod  46292  stoweidlem35  46346  stoweidlem59  46370  fourierdlem31  46449  subsaliuncllem  46668  subsaliuncl  46669  iundjiun  46771  hoiprodcl2  46866  ovn0lem  46876  hoidmvlelem3  46908  smflimlem1  47082  smflimlem2  47083  smflimlem3  47084  fundcmpsurinjlem2  47712  sprval  47792  prprval  47827  rmsupp0  48681  lincop  48721  lcoc0  48735  nelsubclem  49379