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  7442  ovmpt3rabdm  7628  offveqb  7660  epweon  7731  exse2  7873  xpexgALT  7939  opabn1stprc  8016  mpoexg  8034  boxriin  8890  fisupg  9211  fisup2g  9396  fisupcl  9397  fiinfg  9428  fiinf2g  9429  ordtypelem8  9454  wemapso2  9482  cantnflem1  9618  r1val1  9715  updjud  9863  dfac12k  10077  compssiso  10303  axcclem  10386  ondomon  10492  tskuni  10712  pinq  10856  supexpr  10983  dedekind  11313  supadd  12127  supmullem2  12130  zsupss  12872  qextlt  13139  qextle  13140  xrsupsslem  13243  xrinfmsslem  13244  supxrpnf  13254  ssnn0fi  13926  recan  15279  climconst  15485  sumeq2sdvOLD  15646  dvdsext  16267  smupvallem  16429  smumullem  16438  pc11  16827  prmreclem4  16866  vdwmc2  16926  vdwlem8  16935  vdwlem13  16940  cshwsex  17047  cshws0  17048  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdshom  17406  imasplusg  17456  imasmulr  17457  imasip  17460  imasaddvallem  17468  imasvscaf  17478  quslem  17482  divsfval  17486  mrcuni  17562  catideu  17616  homfeqd  17636  comfeqd  17648  2oppccomf  17666  catcoppccl  18059  lublecllem  18299  pmtrrn  19371  pmtrfrn  19372  gsummptif1n0  19880  ip2eq  21595  frlmup4  21743  evlseu  22023  pmatcollpw2lem  22697  basdif0  22873  clsval2  22970  neif  23020  ordtbaslem  23108  ordtrest2lem  23123  lmconst  23181  cndis  23211  pnrmopn  23263  cmpfi  23328  finptfin  23438  comppfsc  23452  ptbasfi  23501  pttoponconst  23517  ptcnplem  23541  pthaus  23558  xkoptsub  23574  xkopt  23575  nrmr0reg  23669  ordthmeolem  23721  fbssfi  23757  filconn  23803  hausflim  23901  cnpflf  23921  fclscf  23945  cnpfcf  23961  alexsublem  23964  ptcmplem2  23973  ptcmplem3  23974  tsmsfbas  24048  eltsms  24053  utopbas  24156  isucn2  24199  psmetutop  24488  nrginvrcn  24613  lebnumlem3  24895  fmcfil  25205  ovolicc2lem4  25454  mbfconst  25567  i1fmul  25630  itg2const  25674  itg2cnlem2  25696  itgle  25744  ibladdlem  25754  iblabs  25763  iblabsr  25764  iblmulc2  25765  bddmulibl  25773  bddiblnc  25776  ellimc2  25811  limcnlp  25812  c1lip1  25935  itgpowd  25990  ply1nzb  26061  ulm0  26333  itgulm2  26351  dchrhash  27215  lgsquadlem2  27325  2sqlem10  27372  dchrisum  27436  rpvmasum2  27456  pntlemj  27547  bday0b  27779  axcontlem12  28955  nbgr0edg  29337  rusgr1vtx  29569  uspgr2wlkeq2  29627  clwwlknondisj  30090  ip2eqi  30835  ubthlem1  30849  hial2eq  31085  pjnmopi  32127  ssmd1  32290  chrelat2i  32344  xrofsup  32740  prodindf  32836  ordtrest2NEWlem  33905  truae  34226  mbfmcst  34243  mbfmcnt  34252  dya2iocuni  34267  0rrv  34435  hashreprin  34604  reprgt  34605  breprexplemc  34616  breprexp  34617  circlemeth  34624  hgt750lema  34641  vonf1owev  35088  wevgblacfn  35089  cvmliftlem15  35278  satf0suclem  35355  fmla0disjsuc  35378  fmlasucdisj  35379  neibastop2lem  36341  tailf  36356  filnetlem4  36362  fin2so  37594  matunitlindflem1  37603  matunitlindflem2  37604  poimirlem26  37633  poimirlem28  37635  ismblfin  37648  cnambfre  37655  itg2addnclem  37658  itg2addnc  37661  itg2gt0cn  37662  ibladdnclem  37663  iblabsnc  37671  iblmulc2nc  37672  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  frinfm  37722  sdclem1  37730  ssbnd  37775  rngoueqz  37927  lssatle  39001  ltrneq2  40135  tendoeq2  40761  lcmineqlem12  42021  hbtlem7  43107  trclrelexplem  43693  rfovcnvf1od  43986  dssmapf1od  44003  neik0pk1imk0  44029  collexd  44239  sswfaxreg  44970  omssaxinf2  44971  prodeq2ad  45583  0cnv  45733  itgperiod  45972  stoweidlem35  46026  stoweidlem59  46050  fourierdlem31  46129  subsaliuncllem  46348  subsaliuncl  46349  iundjiun  46451  hoiprodcl2  46546  ovn0lem  46556  hoidmvlelem3  46588  smflimlem1  46762  smflimlem2  46763  smflimlem3  46764  fundcmpsurinjlem2  47393  sprval  47473  prprval  47508  rmsupp0  48349  lincop  48390  lcoc0  48404  nelsubclem  49049