MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspc Unicode version

Theorem rspc 3204
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
Hypotheses
Ref Expression
rspc.1
rspc.2
Assertion
Ref Expression
rspc
Distinct variable groups:   ,   ,

Proof of Theorem rspc
StepHypRef Expression
1 df-ral 2812 . 2
2 nfcv 2619 . . . 4
3 nfv 1707 . . . . 5
4 rspc.1 . . . . 5
53, 4nfim 1920 . . . 4
6 eleq1 2529 . . . . 5
7 rspc.2 . . . . 5
86, 7imbi12d 320 . . . 4
92, 5, 8spcgf 3189 . . 3
109pm2.43a 49 . 2
111, 10syl5bi 217 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  F/wnf 1616  e.wcel 1818  A.wral 2807
This theorem is referenced by:  rspcv  3206  rspc2  3218  disjxiun  4449  pofun  4821  fmptcof  6065  fliftfuns  6212  ofmpteq  6558  qliftfuns  7417  xpf1o  7699  iunfi  7828  iundom2g  8936  lble  10520  rlimcld2  13401  sumeq2ii  13515  summolem3  13536  zsum  13540  fsum  13542  fsumf1o  13545  sumss2  13548  fsumcvg2  13549  fsumadd  13561  isummulc2  13577  fsum2dlem  13585  fsumcom2  13589  fsumshftm  13596  fsum0diag2  13598  fsummulc2  13599  fsum00  13612  fsumabs  13615  fsumrelem  13621  fsumrlim  13625  fsumo1  13626  o1fsum  13627  fsumiun  13635  isumshft  13651  prodeq2ii  13720  prodmolem3  13740  zprod  13744  fprod  13748  fprodf1o  13753  prodss  13754  fprodser  13756  fprodmul  13765  fproddiv  13766  fprodm1s  13774  fprodp1s  13775  fprodabs  13778  fprod2dlem  13784  fprodcom2  13788  fprodefsum  13830  pcmpt  14411  invfuc  15343  dprd2d2  17093  txcnp  20121  ptcnplem  20122  prdsdsf  20870  prdsxmet  20872  fsumcn  21374  ovolfiniun  21912  ovoliunnul  21918  volfiniun  21957  iunmbl  21963  limciun  22298  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlim  22432  dvfsumrlim2  22433  dvfsum2  22435  itgsubst  22450  fsumvma  23488  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  chirred  27314  voliune  28201  volfiniune  28202  tfisg  29284  ptrest  30048  mzpsubst  30681  rabdiophlem2  30735  etransclem48  32065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111
  Copyright terms: Public domain W3C validator