Theorem ralrimivw 3125

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 3120	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  3154  r19.37v  3155  r19.27v  3158  r19.28v  3160  2rmorex  3714  2reurex  3720  riinrab  5033  exse  5579  mpoeq12  7422  ovmpt3rabdm  7608  offveqb  7640  epweon  7711  exse2  7850  xpexgALT  7916  opabn1stprc  7993  mpoexg  8011  boxriin  8867  fisupg  9177  fisup2g  9359  fisupcl  9360  fiinfg  9391  fiinf2g  9392  ordtypelem8  9417  wemapso2  9445  cantnflem1  9585  r1val1  9682  updjud  9830  dfac12k  10042  compssiso  10268  axcclem  10351  ondomon  10457  tskuni  10677  pinq  10821  supexpr  10948  dedekind  11279  supadd  12093  supmullem2  12096  zsupss  12838  qextlt  13105  qextle  13106  xrsupsslem  13209  xrinfmsslem  13210  supxrpnf  13220  ssnn0fi  13892  recan  15244  climconst  15450  sumeq2sdvOLD  15611  dvdsext  16232  smupvallem  16394  smumullem  16403  pc11  16792  prmreclem4  16831  vdwmc2  16891  vdwlem8  16900  vdwlem13  16905  cshwsex  17012  cshws0  17013  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  imasplusg  17421  imasmulr  17422  imasip  17425  imasaddvallem  17433  imasvscaf  17443  quslem  17447  divsfval  17451  mrcuni  17527  catideu  17581  homfeqd  17601  comfeqd  17613  2oppccomf  17631  catcoppccl  18024  lublecllem  18264  pmtrrn  19336  pmtrfrn  19337  gsummptif1n0  19845  ip2eq  21560  frlmup4  21708  evlseu  21988  pmatcollpw2lem  22662  basdif0  22838  clsval2  22935  neif  22985  ordtbaslem  23073  ordtrest2lem  23088  lmconst  23146  cndis  23176  pnrmopn  23228  cmpfi  23293  finptfin  23403  comppfsc  23417  ptbasfi  23466  pttoponconst  23482  ptcnplem  23506  pthaus  23523  xkoptsub  23539  xkopt  23540  nrmr0reg  23634  ordthmeolem  23686  fbssfi  23722  filconn  23768  hausflim  23866  cnpflf  23886  fclscf  23910  cnpfcf  23926  alexsublem  23929  ptcmplem2  23938  ptcmplem3  23939  tsmsfbas  24013  eltsms  24018  utopbas  24121  isucn2  24164  psmetutop  24453  nrginvrcn  24578  lebnumlem3  24860  fmcfil  25170  ovolicc2lem4  25419  mbfconst  25532  i1fmul  25595  itg2const  25639  itg2cnlem2  25661  itgle  25709  ibladdlem  25719  iblabs  25728  iblabsr  25729  iblmulc2  25730  bddmulibl  25738  bddiblnc  25741  ellimc2  25776  limcnlp  25777  c1lip1  25900  itgpowd  25955  ply1nzb  26026  ulm0  26298  itgulm2  26316  dchrhash  27180  lgsquadlem2  27290  2sqlem10  27337  dchrisum  27401  rpvmasum2  27421  pntlemj  27512  bday0b  27745  axcontlem12  28924  nbgr0edg  29306  rusgr1vtx  29538  uspgr2wlkeq2  29596  clwwlknondisj  30059  ip2eqi  30804  ubthlem1  30818  hial2eq  31054  pjnmopi  32096  ssmd1  32259  chrelat2i  32313  xrofsup  32719  prodindf  32815  extdgfialglem2  33676  ordtrest2NEWlem  33905  truae  34226  mbfmcst  34243  mbfmcnt  34252  dya2iocuni  34267  0rrv  34435  hashreprin  34604  reprgt  34605  breprexplemc  34616  breprexp  34617  circlemeth  34624  hgt750lema  34641  fineqvnttrclselem1  35090  fineqvnttrclse  35093  vonf1owev  35101  wevgblacfn  35102  cvmliftlem15  35291  satf0suclem  35368  fmla0disjsuc  35391  fmlasucdisj  35392  neibastop2lem  36354  tailf  36369  filnetlem4  36375  fin2so  37607  matunitlindflem1  37616  matunitlindflem2  37617  poimirlem26  37646  poimirlem28  37648  ismblfin  37661  cnambfre  37668  itg2addnclem  37671  itg2addnc  37674  itg2gt0cn  37675  ibladdnclem  37676  iblabsnc  37684  iblmulc2nc  37685  ftc1anclem6  37698  ftc1anclem7  37699  ftc1anclem8  37700  ftc1anc  37701  frinfm  37735  sdclem1  37743  ssbnd  37788  rngoueqz  37940  lssatle  39014  ltrneq2  40147  tendoeq2  40773  lcmineqlem12  42033  hbtlem7  43118  trclrelexplem  43704  rfovcnvf1od  43997  dssmapf1od  44014  neik0pk1imk0  44040  collexd  44250  sswfaxreg  44981  omssaxinf2  44982  prodeq2ad  45593  0cnv  45743  itgperiod  45982  stoweidlem35  46036  stoweidlem59  46060  fourierdlem31  46139  subsaliuncllem  46358  subsaliuncl  46359  iundjiun  46461  hoiprodcl2  46556  ovn0lem  46566  hoidmvlelem3  46598  smflimlem1  46772  smflimlem2  46773  smflimlem3  46774  fundcmpsurinjlem2  47403  sprval  47483  prprval  47518  rmsupp0  48372  lincop  48413  lcoc0  48427  nelsubclem  49072