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

Theorem rspccv 3207
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
Hypothesis
Ref Expression
rspcv.1
Assertion
Ref Expression
rspccv
Distinct variable groups:   ,   ,   ,

Proof of Theorem rspccv
StepHypRef Expression
1 rspcv.1 . . 3
21rspcv 3206 . 2
32com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  A.wral 2807
This theorem is referenced by:  elinti  4295  fvn0ssdmfun  6022  dff3  6044  2fvcoidd  6200  ofrval  6550  limsuc  6684  limuni3  6687  frxp  6910  smo11  7054  odi  7247  supub  7939  suplub  7940  elirrv  8044  dfom3  8085  noinfep  8097  oemapvali  8124  tcrank  8323  infxpenlem  8412  alephle  8490  dfac5lem5  8529  dfac2  8532  cofsmo  8670  coftr  8674  infpssrlem4  8707  isf34lem6  8781  axcc2lem  8837  domtriomlem  8843  axdc2lem  8849  axdc3lem2  8852  axdc4lem  8856  ac5b  8879  zorn2lem2  8898  zorn2lem6  8902  pwcfsdom  8979  inar1  9174  grupw  9194  grupr  9196  gruurn  9197  grothpw  9225  grothpwex  9226  axgroth6  9227  grothomex  9228  nqereu  9328  supsrlem  9509  axpre-sup  9567  dedekind  9765  dedekindle  9766  supmullem1  10534  supmul  10536  peano5nni  10564  dfnn2  10574  peano5uzi  10976  zindd  10990  1arith  14445  ramcl  14547  clatleglb  15756  pslem  15836  mndassOLD  15932  cygabl  16893  eqcoe1ply1eq  18339  psgndiflemA  18637  mvmumamul1  19056  smadiadetlem0  19163  chpscmat  19343  basis2  19452  tg2  19466  clsndisj  19576  cnpimaex  19757  t1sncld  19827  regsep  19835  nrmsep3  19856  cmpsub  19900  2ndc1stc  19952  refssex  20012  ptfinfin  20020  txcnpi  20109  txcmplem1  20142  tx1stc  20151  filss  20354  ufilss  20406  fclsopni  20516  fclsrest  20525  alexsubb  20546  alexsubALTlem2  20548  alexsubALTlem4  20550  ghmcnp  20613  qustgplem  20619  mopni  20995  metrest  21027  metcnpi  21047  metcnpi2  21048  cfilucfilOLD  21072  cfilucfil  21073  nmolb  21224  nmoleub2lem2  21599  ovoliunlem1  21913  ovolicc2lem3  21930  mblsplit  21943  fta1b  22570  plycj  22674  mtest  22799  sqfpc  23411  ostth2lem2  23819  ostth3  23823  vdiscusgra  24921  rusgranumwwlkl1  24946  usgn0fidegnn0  25029  numclwwlk1  25098  lpni  25181  nvz  25572  ubthlem2  25787  chcompl  26160  ocin  26214  hmopidmchi  27070  dmdmd  27219  dmdbr5  27227  mdsl1i  27240  sigaclci  28132  lgamgulmlem1  28571  kur14lem9  28658  sconpht  28674  cvmsdisj  28715  untelirr  29080  untsucf  29082  dfon2lem4  29218  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  wfrlem9  29351  frrlem5e  29395  sltval2  29416  heibor1lem  30305  heiborlem4  30310  heiborlem6  30312  stoweid  31845  bnj23  33771  atlex  35041  psubspi  35471  elpcliN  35617  ldilval  35837  trlord  36295  tendotp  36487  hdmapval2  37562  pwelg  37745
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