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

Theorem rspcv 3058
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcv  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 1672 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3056 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-v 2964
This theorem is referenced by:  rspccv  3059  rspcva  3060  rspccva  3061  rspc3v  3071  rr19.3v  3090  rr19.28v  3091  rspsbc  3264  intmin  4136  ralxfrALT  4499  somo  4662  fr2nr  4685  nvocnv  5975  weniso  6032  knatar  6035  grprinvlem  6290  grprinvd  6291  caofref  6335  fr3nr  6380  limuni3  6452  tfinds  6459  funcnvuni  6519  onnseq  6791  smo11  6811  tfrlem1  6821  tfrlem5  6825  tfrlem9  6830  tz7.49  6886  omeulem1  7009  oeordi  7014  nneneq  7482  frfi  7545  unblem2  7553  unbnn2  7557  xpfi  7571  ordiso2  7717  ordtypelem6  7725  ordtypelem7  7726  cantnflem1c  7883  cantnflem1  7885  cantnflem1cOLD  7906  cantnflem1OLD  7908  rankunb  8045  tcrank  8079  carduni  8139  dfac8alem  8187  acni  8203  alephinit  8253  aceq3lem  8278  dfac5  8286  dfac12lem2  8301  dfac12r  8303  dfac12k  8304  pwsdompw  8361  cflm  8407  fin1ai  8450  fin2i  8452  isfin2-2  8476  fin23lem17  8495  fin23lem39  8507  isf32lem1  8510  isf32lem2  8511  isf34lem4  8534  hsmexlem4  8586  axcc3  8595  domtriomlem  8599  axdc3lem2  8608  axdc4lem  8612  axcclem  8614  ttukeylem5  8670  ttukeylem6  8671  axdclem  8676  alephval2  8724  canth4  8802  pwfseqlem5  8818  winainflem  8848  wununi  8861  wunpw  8862  eltskm  8998  dedekind  9521  squeeze0  10223  lbreu  10268  nnsub  10348  ublbneg  10927  zsupss  10932  uzwo3  10936  zmax  10938  zbtwnre  10939  xrub  11262  fzrevral  11528  axdc4uzlem  11788  seqcl2  11808  seqcl  11810  seqf  11811  seqfveq2  11812  seqfveq  11814  seqshft2  11816  monoord  11820  monoord2  11821  sermono  11822  seqsplit  11823  seqcaopr3  11825  seqid  11835  seqid2  11836  seqhomo  11837  seqz  11838  discr1  11984  discr  11985  faclbnd4lem4  12056  hashbclem  12189  wrdind  12355  wrd2ind  12356  recan  12808  cau3lem  12826  caubnd2  12829  limsupgre  12943  climi  12972  rlimi  12975  rlimclim1  13007  rlimclim  13008  climrlim2  13009  climshftlem  13036  rlimcld2  13040  rlimcn1  13050  climcn1  13053  subcn2  13056  isercoll  13129  isercoll2  13130  climcau  13132  caucvgrlem  13134  caucvgb  13141  serf0  13142  iseraltlem2  13144  iseraltlem3  13145  iseralt  13146  fsumm1  13204  fsum1p  13206  fsumcom2  13225  fsumge1  13243  fsumtscopo  13248  fsumtscopo2  13249  fsumparts  13252  o1fsum  13259  isum1p  13287  isumnn0nn  13288  isumrpcl  13289  climcndslem1  13295  climcndslem2  13296  climcnds  13297  cvgrat  13326  mertenslem1  13327  mertens  13329  sqr2irr  13514  ndvdssub  13594  prmind2  13757  nprm  13760  dvdsprm  13768  coprm  13769  pcmpt  13937  pcmpt2  13938  pcmptdvds  13939  pcfac  13944  prmpwdvds  13948  unbenlem  13952  prmreclem4  13963  prmreclem5  13964  vdwlem1  14025  vdwlem2  14026  vdwlem9  14033  vdwlem10  14034  vdwlem13  14037  vdwnnlem1  14039  rami  14059  ramcl  14073  catidex  14595  catideu  14596  iscatd2  14602  catlid  14604  catrid  14605  subcidcl  14737  funcid  14763  yonedalem4c  15070  yonffthlem  15075  isdrs2  15092  lublecllem  15141  lubun  15276  poslubmo  15299  posglbmo  15300  grpidd2  15555  mulgsubcl  15621  issubg4  15680  ghmf1  15755  fislw  16104  efgi  16196  efgi2  16202  efgsdmi  16209  efgsrel  16211  gexexlem  16314  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsummhm2  16411  gsummhm2OLD  16412  dprdcntz  16466  dprddisj  16467  dprdss  16500  dprd2dlem2  16513  dprd2da  16515  dpjrid  16535  ablfac1eu  16548  pgpfac1lem1  16549  pgpfaclem2  16557  issrngd  16870  islmodd  16878  islmhm2  17041  islbs2  17157  lbsextlem4  17164  rrgeq0i  17282  mvrf1  17432  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  subrgasclcl  17513  prmirredlem  17759  prmirredlemOLD  17762  ip2eq  17924  frlmphl  18048  mdetralt  18256  isclo2  18534  lmcvg  18708  cnpnei  18710  iscncl  18715  cncls  18720  lmss  18744  lmff  18747  cnt0  18792  isnrm2  18804  cnrmi  18806  isreg2  18823  cmpcov  18834  tgcmp  18846  uncmp  18848  fiuncmp  18849  bwthOLD  18856  dfcon2  18865  1stcclb  18890  1stcfb  18891  2ndcctbss  18901  1stcelcls  18907  restnlly  18928  islly2  18930  lly1stc  18942  kgeni  18952  kgencn2  18972  ptpjpre1  18986  ptbasfi  18996  ptpjopn  19027  dfac14  19033  txtube  19055  txlm  19063  cnmpt11  19078  cnmpt21  19086  cnmptkp  19095  cnmptk1p  19100  qtopomap  19133  qtopcmap  19134  kqfvima  19145  kqt0lem  19151  isr0  19152  nrmr0reg  19164  fgss2  19289  isufil2  19323  cfinufil  19343  flimopn  19390  fbflim2  19392  flimcf  19397  flfneii  19407  cnpflf  19416  fclssscls  19433  fclsnei  19434  fclsrest  19439  fclscf  19440  flimfnfcls  19443  fclscmp  19445  isfcf  19449  fcfnei  19450  alexsubALTlem3  19463  alexsubALTlem4  19464  alexsubALT  19465  ptcmplem3  19468  tgpt0  19531  tsmsi  19546  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmsxplem1  19569  tsmsxplem2  19570  tsmsxp  19571  ustincl  19624  ustdiag  19625  ustinvel  19626  ustexhalf  19627  isucn2  19696  ucnima  19698  ucncn  19702  cfiluexsm  19707  psmet0  19726  imasdsf1olem  19790  prdsbl  19908  metss  19925  comet  19930  metcnp3  19957  isngp4  20045  nmoi  20149  mulc1cncf  20323  cncfco  20325  cnheiborlem  20368  cnheibor  20369  bndth  20372  lebnumii  20380  nmoleub2lem2  20513  nmoleub3  20516  ipcau2  20591  tchcphlem1  20592  tchcphlem2  20593  lmmcvg  20614  iscfil3  20626  iscau2  20630  iscau4  20632  cmetcaulem  20641  iscmet3lem1  20644  iscmet3lem2  20645  equivcfil  20652  equivcau  20653  lmcau  20665  pjthlem1  20766  pjthlem2  20767  ivthlem1  20777  ivthlem2  20778  ivthlem3  20779  ivth2  20781  ivthle  20782  ivthle2  20783  ivthicc  20784  ovoliunlem1  20827  ovolshftlem1  20834  ovolscalem1  20838  ovolicc2lem3  20844  ovolicc2lem4  20845  ovolicc2  20847  volsup  20879  dyadmbl  20922  vitalilem2  20931  vitalilem3  20932  mbfdm  20948  ismbf  20950  ismbf3d  20974  cncombf  20978  itg2seq  21062  itg2monolem2  21071  itg2monolem3  21072  itg2mono  21073  iblitg  21088  itgconst  21138  itgfsum  21146  limcvallem  21188  ellimc3  21196  cnlimci  21206  cnmptlimc  21207  dvferm1lem  21298  dvferm1  21299  dvferm2lem  21300  dvferm2  21301  dvlipcn  21308  dvle  21321  lhop1lem  21327  lhop1  21328  dvfsumge  21336  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumlem4  21343  dvfsum2  21348  ftc1a  21351  ftc1lem4  21353  itgsubstlem  21362  fta1glem2  21523  fta1g  21524  plyeq0lem  21563  dgrcolem2  21626  dgrco  21627  plydivlem4  21647  plydivex  21648  fta1lem  21658  fta1  21659  vieta1lem2  21662  vieta1  21663  aalioulem2  21684  aalioulem4  21686  tayl0  21712  ulmi  21736  ulmclm  21737  ulmshftlem  21739  ulmcaulem  21744  ulmcau  21745  ulmcn  21749  ulmdvlem1  21750  ulmdvlem3  21752  ulmdv  21753  pserulm  21772  efif1olem4  21886  rlimcnp  22244  rlimcnp2  22245  xrlimcnp  22247  cxploglim  22256  scvxcvx  22264  wilthlem2  22292  ftalem3  22297  fsumdvdscom  22410  musumsum  22417  chtub  22436  fsumvma  22437  perfectlem2  22454  dchrelbas3  22462  dchrelbasd  22463  dchrn0  22474  dchrptlem2  22489  lgsval2lem  22530  lgsdirnn0  22563  lgsdinn0  22564  2sqlem6  22593  2sqlem10  22598  dchrisumlema  22622  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrmusum2  22628  dchrvmasumlem2  22632  dchrvmasumlem3  22633  dchrvmasumiflem1  22635  dchrisum0flblem2  22643  dchrisum0flb  22644  dchrisum0lem1b  22649  dchrisum0lem2  22652  2vmadivsumlem  22674  chpdifbndlem1  22687  selberg3lem1  22691  selberg4lem1  22694  pntrsumbnd2  22701  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntpbnd1  22720  pntibndlem2  22725  pntibndlem3  22726  pntibnd  22727  pntlemn  22734  pntlemj  22737  pntlemi  22738  pntlemo  22741  pntlem3  22743  pntleml  22745  ostth2lem1  22752  ostth2lem2  22768  ostth3  22772  brbtwn2  22974  colinearalg  22979  axcontlem4  23036  nbgra0nb  23163  nbgrassovt  23169  cusgrarn  23190  usgrasscusgra  23214  isgrpo  23506  isgrp2d  23545  opidon  23632  exidu1  23636  rngoideu  23694  blocnilem  24027  ip2eqi  24080  ubthlem1  24094  minvecolem3  24100  htthlem  24142  hial0  24327  hial02  24328  hial2eq  24331  ocorth  24517  occllem  24529  pjhthlem1  24617  h1de2i  24779  pjjsi  24926  lnopunilem1  25237  lnophmlem1  25243  nmcexi  25253  riesz4i  25290  mdi  25522  mdbr3  25524  mdbr4  25525  dmdi  25529  dmdbr3  25532  dmdbr4  25533  dmdi4  25534  mdslmd1i  25556  atss  25573  atom1d  25580  atmd  25626  sumdmdlem2  25646  cdj1i  25660  cdj3i  25668  nn0min  25913  archiabllem1a  26032  archiabllem2a  26035  archiabl  26039  srgrz  26061  srgisid  26062  rngurd  26109  isarchiofld  26138  fmcncfil  26215  sigaclcu  26414  unelsiga  26431  measvun  26477  mbfmcnvima  26526  sibfima  26572  signstfvneq0  26821  lgamgulmlem5  26867  lgambdd  26871  lgamcvglem  26874  derangenlem  26907  subfacp1lem5  26920  subfacp1lem6  26921  rescon  26983  cvmcov  27000  cvmliftlem3  27024  cvmlift2lem10  27049  cvmliftphtlem  27054  ghomgrpilem1  27151  ghomf1olem  27160  clim2prod  27250  ntrivcvgfvn0  27261  fprodm1  27324  fprod1p  27325  fprodcom2  27342  dfon2lem6  27448  poseq  27561  soseq  27562  nocvxminlem  27678  nobndlem6  27685  fin2so  28260  mbfresfi  28282  ftc1cnnclem  28309  opnrebl2  28360  nn0prpwlem  28361  nn0prpw  28362  comppfsc  28423  neibastop2lem  28425  neibastop2  28426  filnetlem4  28446  seqpo  28487  incsequz  28488  mettrifi  28497  geomcau  28499  caushft  28501  sstotbnd2  28517  equivtotbnd  28521  totbndbnd  28532  ismtybndlem  28549  heibor1lem  28552  bfplem2  28566  isdrngo2  28608  unichnidl  28675  incssnn0  28892  lnmlssfg  29278  unxpwdom3  29293  fnchoice  29596  wwlknredwwlkn  30204  clwwlkf1  30304  clwwlkext2edg  30310  wwlkextproplem2  30407  3cyclfrgrarn1  30450  n4cyclfrgra  30456  frgrawopreglem4  30486  frgrawopreg1  30489  frgrawopreg2  30490  extwwlkfablem2  30517  lcosslsp  30681  linindslinci  30691  lindslinindsimp1  30700  ldepsnlinclem1  30756  ldepsnlinclem2  30757  lsat0cv  32251  lcvexchlem4  32255  lcvexchlem5  32256  eqlkr3  32319  lub0N  32407  glb0N  32411  cvrnbtwn  32489  ltrneq2  33365  trlval2  33380  lpolsatN  34706  lpolpolsatN  34707  hdmap14lem12  35100
  Copyright terms: Public domain W3C validator