Theorem ralrimivw 3160

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 3155	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  r19.21v  3189  r19.37v  3190  r19.27v  3193  r19.28v  3195  2rmorex  3716  2reurex  3722  riinrab  5049  exse  5620  mpoeq12  7485  ovmpt3rabdm  7671  offveqb  7703  epweon  7772  exse2  7912  xpexgALT  7976  opabn1stprc  8053  mpoexg  8071  boxriin  8936  fisupg  9246  fisup2g  9427  fisupcl  9428  fiinfg  9459  fiinf2g  9460  ordtypelem8  9485  wemapso2  9513  cantnflem1  9656  r1val1  9756  updjud  9927  dfac12k  10138  compssiso  10364  axcclem  10447  ondomon  10553  tskuni  10774  pinq  10918  supexpr  11045  dedekind  11379  supadd  12189  supmullem2  12192  zsupss  12967  qextlt  13235  qextle  13236  xrsupsslem  13339  xrinfmsslem  13340  supxrpnf  13350  ssnn0fi  14028  recan  15395  climconst  15601  sumeq2sdvOLD  15762  dvdsext  16385  smupvallem  16547  smumullem  16556  pc11  16946  prmreclem4  16985  vdwmc2  17045  vdwlem8  17054  vdwlem13  17059  cshwsex  17166  cshws0  17167  prdsplusg  17517  prdsmulr  17518  prdsvsca  17519  prdshom  17526  imasplusg  17577  imasmulr  17578  imasip  17581  imasaddvallem  17589  imasvscaf  17599  quslem  17603  divsfval  17607  mrcuni  17683  catideu  17737  homfeqd  17757  comfeqd  17769  2oppccomf  17787  catcoppccl  18180  lublecllem  18420  chnfi  18696  pmtrrn  19533  pmtrfrn  19534  gsummptif1n0  20042  ip2eq  21814  frlmup4  21962  evlseu  22245  pmatcollpw2lem  22945  basdif0  23121  clsval2  23218  neif  23268  ordtbaslem  23356  ordtrest2lem  23371  lmconst  23429  cndis  23459  pnrmopn  23511  cmpfi  23576  finptfin  23686  comppfsc  23700  ptbasfi  23749  pttoponconst  23765  ptcnplem  23789  pthaus  23806  xkoptsub  23822  xkopt  23823  nrmr0reg  23917  ordthmeolem  23969  fbssfi  24005  filconn  24051  hausflim  24149  cnpflf  24169  fclscf  24193  cnpfcf  24209  alexsublem  24212  ptcmplem2  24221  ptcmplem3  24222  tsmsfbas  24296  eltsms  24301  utopbas  24403  isucn2  24446  psmetutop  24735  nrginvrcn  24860  lebnumlem3  25133  fmcfil  25442  ovolicc2lem4  25690  mbfconst  25803  i1fmul  25866  itg2const  25910  itg2cnlem2  25932  itgle  25980  ibladdlem  25990  iblabs  25999  iblabsr  26000  iblmulc2  26001  bddmulibl  26009  bddiblnc  26012  ellimc2  26047  limcnlp  26048  c1lip1  26167  itgpowd  26220  ply1nzb  26291  ulm0  26565  itgulm2  26583  dchrhash  27446  lgsquadlem2  27556  2sqlem10  27603  dchrisum  27667  rpvmasum2  27687  pntlemj  27778  bday0b  28017  axcontlem12  29336  nbgr0edg  29718  rusgr1vtx  29949  uspgr2wlkeq2  30007  clwwlknondisj  30473  ip2eqi  31219  ubthlem1  31233  hial2eq  31469  pjnmopi  32511  ssmd1  32674  chrelat2i  32728  xrofsup  33123  prodindf  33193  selvply1rhmlemb  33918  extdgfialglem2  34092  ordtrest2NEWlem  34321  truae  34642  mbfmcst  34658  mbfmcnt  34667  dya2iocuni  34682  0rrv  34850  hashreprin  35016  reprgt  35017  breprexplemc  35028  breprexp  35029  circlemeth  35036  hgt750lema  35053  fineqvnttrclselem1  35542  fineqvnttrclse  35545  vonf1wev  35600  vonf1owevOLD  35602  wevgblacfn  35603  onvfowev  35608  cvmliftlem15  35798  satf0suclem  35875  fmla0disjsuc  35898  fmlasucdisj  35899  neibastop2lem  36899  tailf  36914  filnetlem4  36920  fin2so  38286  matunitlindflem1  38295  matunitlindflem2  38296  poimirlem26  38325  poimirlem28  38327  ismblfin  38340  cnambfre  38347  itg2addnclem  38350  itg2addnc  38353  itg2gt0cn  38354  ibladdnclem  38355  iblabsnc  38363  iblmulc2nc  38364  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  frinfm  38414  sdclem1  38422  ssbnd  38467  rngoueqz  38619  lssatle  39817  ltrneq2  40950  tendoeq2  41576  lcmineqlem12  42835  hbtlem7  43880  trclrelexplem  44465  rfovcnvf1od  44758  dssmapf1od  44775  neik0pk1imk0  44801  collexd  44995  sswfaxreg  45724  omssaxinf2  45725  prodeq2ad  46336  0cnv  46484  itgperiod  46723  stoweidlem35  46777  stoweidlem59  46801  fourierdlem31  46880  subsaliuncllem  47099  subsaliuncl  47100  iundjiun  47202  hoiprodcl2  47297  ovn0lem  47307  hoidmvlelem3  47339  smflimlem1  47513  smflimlem2  47514  smflimlem3  47515  fundcmpsurinjlem2  48176  sprval  48256  prprval  48291  rmsupp0  49176  lincop  49216  lcoc0  49230  nelsubclem  49873