Theorem ralrimivw 3129

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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 1910

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

This theorem is referenced by:  r19.21v  3158  r19.37v  3159  r19.27v  3164  r19.28v  3166  2rmorex  3722  2reurex  3728  riinrab  5043  exse  5591  mpoeq12  7443  ovmpt3rabdm  7629  offveqb  7661  epweon  7732  exse2  7874  xpexgALT  7940  opabn1stprc  8017  mpoexg  8035  boxriin  8891  fisupg  9212  fisup2g  9397  fisupcl  9398  fiinfg  9429  fiinf2g  9430  ordtypelem8  9455  wemapso2  9483  cantnflem1  9621  r1val1  9718  updjud  9866  dfac12k  10080  compssiso  10306  axcclem  10389  ondomon  10495  tskuni  10715  pinq  10859  supexpr  10986  dedekind  11316  supadd  12130  supmullem2  12133  zsupss  12875  qextlt  13142  qextle  13143  xrsupsslem  13246  xrinfmsslem  13247  supxrpnf  13257  ssnn0fi  13929  recan  15281  climconst  15487  sumeq2sdvOLD  15648  dvdsext  16269  smupvallem  16431  smumullem  16440  pc11  16829  prmreclem4  16868  vdwmc2  16928  vdwlem8  16937  vdwlem13  16942  cshwsex  17049  cshws0  17050  prdsplusg  17399  prdsmulr  17400  prdsvsca  17401  prdshom  17408  imasplusg  17458  imasmulr  17459  imasip  17462  imasaddvallem  17470  imasvscaf  17480  quslem  17484  divsfval  17488  mrcuni  17564  catideu  17618  homfeqd  17638  comfeqd  17650  2oppccomf  17668  catcoppccl  18061  lublecllem  18301  pmtrrn  19373  pmtrfrn  19374  gsummptif1n0  19882  ip2eq  21597  frlmup4  21745  evlseu  22025  pmatcollpw2lem  22699  basdif0  22875  clsval2  22972  neif  23022  ordtbaslem  23110  ordtrest2lem  23125  lmconst  23183  cndis  23213  pnrmopn  23265  cmpfi  23330  finptfin  23440  comppfsc  23454  ptbasfi  23503  pttoponconst  23519  ptcnplem  23543  pthaus  23560  xkoptsub  23576  xkopt  23577  nrmr0reg  23671  ordthmeolem  23723  fbssfi  23759  filconn  23805  hausflim  23903  cnpflf  23923  fclscf  23947  cnpfcf  23963  alexsublem  23966  ptcmplem2  23975  ptcmplem3  23976  tsmsfbas  24050  eltsms  24055  utopbas  24158  isucn2  24201  psmetutop  24490  nrginvrcn  24615  lebnumlem3  24897  fmcfil  25207  ovolicc2lem4  25456  mbfconst  25569  i1fmul  25632  itg2const  25676  itg2cnlem2  25698  itgle  25746  ibladdlem  25756  iblabs  25765  iblabsr  25766  iblmulc2  25767  bddmulibl  25775  bddiblnc  25778  ellimc2  25813  limcnlp  25814  c1lip1  25937  itgpowd  25992  ply1nzb  26063  ulm0  26335  itgulm2  26353  dchrhash  27217  lgsquadlem2  27327  2sqlem10  27374  dchrisum  27438  rpvmasum2  27458  pntlemj  27549  bday0b  27781  axcontlem12  28957  nbgr0edg  29339  rusgr1vtx  29571  uspgr2wlkeq2  29629  clwwlknondisj  30092  ip2eqi  30837  ubthlem1  30851  hial2eq  31087  pjnmopi  32129  ssmd1  32292  chrelat2i  32346  xrofsup  32742  prodindf  32838  ordtrest2NEWlem  33907  truae  34228  mbfmcst  34245  mbfmcnt  34254  dya2iocuni  34269  0rrv  34437  hashreprin  34606  reprgt  34607  breprexplemc  34618  breprexp  34619  circlemeth  34626  hgt750lema  34643  vonf1owev  35090  wevgblacfn  35091  cvmliftlem15  35280  satf0suclem  35357  fmla0disjsuc  35380  fmlasucdisj  35381  neibastop2lem  36343  tailf  36358  filnetlem4  36364  fin2so  37596  matunitlindflem1  37605  matunitlindflem2  37606  poimirlem26  37635  poimirlem28  37637  ismblfin  37650  cnambfre  37657  itg2addnclem  37660  itg2addnc  37663  itg2gt0cn  37664  ibladdnclem  37665  iblabsnc  37673  iblmulc2nc  37674  ftc1anclem6  37687  ftc1anclem7  37688  ftc1anclem8  37689  ftc1anc  37690  frinfm  37724  sdclem1  37732  ssbnd  37777  rngoueqz  37929  lssatle  39003  ltrneq2  40137  tendoeq2  40763  lcmineqlem12  42023  hbtlem7  43109  trclrelexplem  43695  rfovcnvf1od  43988  dssmapf1od  44005  neik0pk1imk0  44031  collexd  44241  sswfaxreg  44972  omssaxinf2  44973  prodeq2ad  45585  0cnv  45735  itgperiod  45974  stoweidlem35  46028  stoweidlem59  46052  fourierdlem31  46131  subsaliuncllem  46350  subsaliuncl  46351  iundjiun  46453  hoiprodcl2  46548  ovn0lem  46558  hoidmvlelem3  46590  smflimlem1  46764  smflimlem2  46765  smflimlem3  46766  fundcmpsurinjlem2  47395  sprval  47475  prprval  47510  rmsupp0  48351  lincop  48392  lcoc0  48406  nelsubclem  49051