Theorem ralrimivw 3167

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  r19.21v  3196  r19.37v  3197  r19.27v  3200  r19.28v  3202  2rmorex  3724  2reurex  3730  riinrab  5052  exse  5622  mpoeq12  7484  ovmpt3rabdm  7670  offveqb  7702  epweon  7774  exse2  7914  xpexgALT  7978  opabn1stprc  8055  mpoexg  8073  boxriin  8938  fisupg  9248  fisup2g  9429  fisupcl  9430  fiinfg  9461  fiinf2g  9462  ordtypelem8  9487  wemapso2  9515  cantnflem1  9658  r1val1  9758  updjud  9920  dfac12k  10131  compssiso  10358  axcclem  10441  ondomon  10547  tskuni  10768  pinq  10912  supexpr  11039  dedekind  11373  supadd  12183  supmullem2  12186  zsupss  12961  qextlt  13229  qextle  13230  xrsupsslem  13333  xrinfmsslem  13334  supxrpnf  13344  ssnn0fi  14021  recan  15388  climconst  15594  sumeq2sdvOLD  15755  dvdsext  16379  smupvallem  16541  smumullem  16550  pc11  16940  prmreclem4  16979  vdwmc2  17039  vdwlem8  17048  vdwlem13  17053  cshwsex  17160  cshws0  17161  prdsplusg  17511  prdsmulr  17512  prdsvsca  17513  prdshom  17520  imasplusg  17571  imasmulr  17572  imasip  17575  imasaddvallem  17583  imasvscaf  17593  quslem  17597  divsfval  17601  mrcuni  17677  catideu  17731  homfeqd  17751  comfeqd  17763  2oppccomf  17781  catcoppccl  18174  lublecllem  18414  chnfi  18690  pmtrrn  19527  pmtrfrn  19528  gsummptif1n0  20036  ip2eq  21772  frlmup4  21920  evlseu  22203  pmatcollpw2lem  22903  basdif0  23079  clsval2  23176  neif  23226  ordtbaslem  23314  ordtrest2lem  23329  lmconst  23387  cndis  23417  pnrmopn  23469  cmpfi  23534  finptfin  23644  comppfsc  23658  ptbasfi  23707  pttoponconst  23723  ptcnplem  23747  pthaus  23764  xkoptsub  23780  xkopt  23781  nrmr0reg  23875  ordthmeolem  23927  fbssfi  23963  filconn  24009  hausflim  24107  cnpflf  24127  fclscf  24151  cnpfcf  24167  alexsublem  24170  ptcmplem2  24179  ptcmplem3  24180  tsmsfbas  24254  eltsms  24259  utopbas  24361  isucn2  24404  psmetutop  24693  nrginvrcn  24818  lebnumlem3  25091  fmcfil  25400  ovolicc2lem4  25648  mbfconst  25761  i1fmul  25824  itg2const  25868  itg2cnlem2  25890  itgle  25938  ibladdlem  25948  iblabs  25957  iblabsr  25958  iblmulc2  25959  bddmulibl  25967  bddiblnc  25970  ellimc2  26005  limcnlp  26006  c1lip1  26125  itgpowd  26178  ply1nzb  26249  ulm0  26520  itgulm2  26538  dchrhash  27401  lgsquadlem2  27511  2sqlem10  27558  dchrisum  27622  rpvmasum2  27642  pntlemj  27733  bday0b  27972  axcontlem12  29266  nbgr0edg  29648  rusgr1vtx  29879  uspgr2wlkeq2  29937  clwwlknondisj  30403  ip2eqi  31149  ubthlem1  31163  hial2eq  31399  pjnmopi  32441  ssmd1  32604  chrelat2i  32658  xrofsup  33053  prodindf  33123  selvply1rhmlemb  33854  extdgfialglem2  34028  ordtrest2NEWlem  34257  truae  34578  mbfmcst  34594  mbfmcnt  34603  dya2iocuni  34618  0rrv  34786  hashreprin  34952  reprgt  34953  breprexplemc  34964  breprexp  34965  circlemeth  34972  hgt750lema  34989  fineqvnttrclselem1  35467  fineqvnttrclse  35470  vonf1wev  35525  vonf1owevOLD  35527  wevgblacfn  35528  onvfowev  35533  cvmliftlem15  35723  satf0suclem  35800  fmla0disjsuc  35823  fmlasucdisj  35824  neibastop2lem  36794  tailf  36809  filnetlem4  36815  fin2so  38181  matunitlindflem1  38190  matunitlindflem2  38191  poimirlem26  38220  poimirlem28  38222  ismblfin  38235  cnambfre  38242  itg2addnclem  38245  itg2addnc  38248  itg2gt0cn  38249  ibladdnclem  38250  iblabsnc  38258  iblmulc2nc  38259  ftc1anclem6  38272  ftc1anclem7  38273  ftc1anclem8  38274  ftc1anc  38275  frinfm  38309  sdclem1  38317  ssbnd  38362  rngoueqz  38514  lssatle  39714  ltrneq2  40847  tendoeq2  41473  lcmineqlem12  42732  hbtlem7  43779  trclrelexplem  44364  rfovcnvf1od  44657  dssmapf1od  44674  neik0pk1imk0  44700  collexd  44894  sswfaxreg  45623  omssaxinf2  45624  prodeq2ad  46235  0cnv  46383  itgperiod  46622  stoweidlem35  46676  stoweidlem59  46700  fourierdlem31  46779  subsaliuncllem  46998  subsaliuncl  46999  iundjiun  47101  hoiprodcl2  47196  ovn0lem  47206  hoidmvlelem3  47238  smflimlem1  47412  smflimlem2  47413  smflimlem3  47414  fundcmpsurinjlem2  48072  sprval  48152  prprval  48187  rmsupp0  49068  lincop  49108  lcoc0  49122  nelsubclem  49765