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

Theorem rspcv 3165
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 1674 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3163 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370    e. wcel 1758   A.wral 2795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-v 3070
This theorem is referenced by:  rspccv  3166  rspcva  3167  rspccva  3168  rspc3v  3179  rr19.3v  3198  rr19.28v  3199  rspsbc  3374  intmin  4246  ralxfrALT  4609  somo  4773  fr2nr  4796  nvocnv  6087  weniso  6144  knatar  6147  grprinvlem  6401  grprinvd  6402  caofref  6446  fr3nr  6491  limuni3  6563  tfinds  6570  funcnvuni  6630  onnseq  6905  smo11  6925  tfrlem1  6935  tfrlem5  6939  tfrlem9  6944  tz7.49  7000  omeulem1  7121  oeordi  7126  nneneq  7594  frfi  7658  unblem2  7666  unbnn2  7670  xpfi  7684  ordiso2  7830  ordtypelem6  7838  ordtypelem7  7839  cantnflem1c  7996  cantnflem1  7998  cantnflem1cOLD  8019  cantnflem1OLD  8021  rankunb  8158  tcrank  8192  carduni  8252  dfac8alem  8300  acni  8316  alephinit  8366  aceq3lem  8391  dfac5  8399  dfac12lem2  8414  dfac12r  8416  dfac12k  8417  pwsdompw  8474  cflm  8520  fin1ai  8563  fin2i  8565  isfin2-2  8589  fin23lem17  8608  fin23lem39  8620  isf32lem1  8623  isf32lem2  8624  isf34lem4  8647  hsmexlem4  8699  axcc3  8708  domtriomlem  8712  axdc3lem2  8721  axdc4lem  8725  axcclem  8727  ttukeylem5  8783  ttukeylem6  8784  axdclem  8789  alephval2  8837  canth4  8915  pwfseqlem5  8931  winainflem  8961  wununi  8974  wunpw  8975  eltskm  9111  dedekind  9634  squeeze0  10336  lbreu  10381  nnsub  10461  ublbneg  11040  zsupss  11045  uzwo3  11049  zmax  11051  zbtwnre  11052  xrub  11375  fzrevral  11645  axdc4uzlem  11905  seqcl2  11925  seqcl  11927  seqf  11928  seqfveq2  11929  seqfveq  11931  seqshft2  11933  monoord  11937  monoord2  11938  sermono  11939  seqsplit  11940  seqcaopr3  11942  seqid  11952  seqid2  11953  seqhomo  11954  seqz  11955  discr1  12101  discr  12102  faclbnd4lem4  12173  hashbclem  12307  wrdind  12473  wrd2ind  12474  recan  12926  cau3lem  12944  caubnd2  12947  limsupgre  13061  climi  13090  rlimi  13093  rlimclim1  13125  rlimclim  13126  climrlim2  13127  climshftlem  13154  rlimcld2  13158  rlimcn1  13168  climcn1  13171  subcn2  13174  isercoll  13247  isercoll2  13248  climcau  13250  caucvgrlem  13252  caucvgb  13259  serf0  13260  iseraltlem2  13262  iseraltlem3  13263  iseralt  13264  fsumm1  13322  fsum1p  13324  fsumcom2  13343  fsumge1  13362  fsumtscopo  13367  fsumtscopo2  13368  fsumparts  13371  o1fsum  13378  isum1p  13406  isumnn0nn  13407  isumrpcl  13408  climcndslem1  13414  climcndslem2  13415  climcnds  13416  cvgrat  13445  mertenslem1  13446  mertens  13448  sqr2irr  13633  ndvdssub  13713  prmind2  13876  nprm  13879  dvdsprm  13887  coprm  13888  pcmpt  14056  pcmpt2  14057  pcmptdvds  14058  pcfac  14063  prmpwdvds  14067  unbenlem  14071  prmreclem4  14082  prmreclem5  14083  vdwlem1  14144  vdwlem2  14145  vdwlem9  14152  vdwlem10  14153  vdwlem13  14156  vdwnnlem1  14158  rami  14178  ramcl  14192  catidex  14714  catideu  14715  iscatd2  14721  catlid  14723  catrid  14724  subcidcl  14856  funcid  14882  yonedalem4c  15189  yonffthlem  15194  isdrs2  15211  lublecllem  15260  lubun  15395  poslubmo  15418  posglbmo  15419  grpidd2  15677  mulgsubcl  15743  issubg4  15802  ghmf1  15877  fislw  16228  efgi  16320  efgi2  16326  efgsdmi  16333  efgsrel  16335  gexexlem  16438  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsummhm2  16539  gsummhm2OLD  16540  dprdcntz  16597  dprddisj  16598  dprdss  16631  dprd2dlem2  16644  dprd2da  16646  dpjrid  16666  ablfac1eu  16679  pgpfac1lem1  16680  pgpfaclem2  16688  srgrz  16732  srglz  16733  srgisid  16734  f1rhm0to0ALT  16935  issrngd  17052  islmodd  17060  islmhm2  17225  islbs2  17341  lbsextlem4  17348  rrgeq0i  17466  mvrf1  17605  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  subrgasclcl  17688  prmirredlem  18026  prmirredlemOLD  18029  ip2eq  18191  frlmphl  18315  mdetralt  18530  isclo2  18808  lmcvg  18982  cnpnei  18984  iscncl  18989  cncls  18994  lmss  19018  lmff  19021  cnt0  19066  isnrm2  19078  cnrmi  19080  isreg2  19097  cmpcov  19108  tgcmp  19120  uncmp  19122  fiuncmp  19123  bwthOLD  19130  dfcon2  19139  1stcclb  19164  1stcfb  19165  2ndcctbss  19175  1stcelcls  19181  restnlly  19202  islly2  19204  lly1stc  19216  kgeni  19226  kgencn2  19246  ptpjpre1  19260  ptbasfi  19270  ptpjopn  19301  dfac14  19307  txtube  19329  txlm  19337  cnmpt11  19352  cnmpt21  19360  cnmptkp  19369  cnmptk1p  19374  qtopomap  19407  qtopcmap  19408  kqfvima  19419  kqt0lem  19425  isr0  19426  nrmr0reg  19438  fgss2  19563  isufil2  19597  cfinufil  19617  flimopn  19664  fbflim2  19666  flimcf  19671  flfneii  19681  cnpflf  19690  fclssscls  19707  fclsnei  19708  fclsrest  19713  fclscf  19714  flimfnfcls  19717  fclscmp  19719  isfcf  19723  fcfnei  19724  alexsubALTlem3  19737  alexsubALTlem4  19738  alexsubALT  19739  ptcmplem3  19742  tgpt0  19805  tsmsi  19820  tsmsgsum  19825  tsmsgsumOLD  19828  tsmsresOLD  19833  tsmsres  19834  tsmsxplem1  19843  tsmsxplem2  19844  tsmsxp  19845  ustincl  19898  ustdiag  19899  ustinvel  19900  ustexhalf  19901  isucn2  19970  ucnima  19972  ucncn  19976  cfiluexsm  19981  psmet0  20000  imasdsf1olem  20064  prdsbl  20182  metss  20199  comet  20204  metcnp3  20231  isngp4  20319  nmoi  20423  mulc1cncf  20597  cncfco  20599  cnheiborlem  20642  cnheibor  20643  bndth  20646  lebnumii  20654  nmoleub2lem2  20787  nmoleub3  20790  ipcau2  20865  tchcphlem1  20866  tchcphlem2  20867  lmmcvg  20888  iscfil3  20900  iscau2  20904  iscau4  20906  cmetcaulem  20915  iscmet3lem1  20918  iscmet3lem2  20919  equivcfil  20926  equivcau  20927  lmcau  20939  pjthlem1  21040  pjthlem2  21041  ivthlem1  21051  ivthlem2  21052  ivthlem3  21053  ivth2  21055  ivthle  21056  ivthle2  21057  ivthicc  21058  ovoliunlem1  21101  ovolshftlem1  21108  ovolscalem1  21112  ovolicc2lem3  21118  ovolicc2lem4  21119  ovolicc2  21121  volsup  21153  dyadmbl  21196  vitalilem2  21205  vitalilem3  21206  mbfdm  21222  ismbf  21224  ismbf3d  21248  cncombf  21252  itg2seq  21336  itg2monolem2  21345  itg2monolem3  21346  itg2mono  21347  iblitg  21362  itgconst  21412  itgfsum  21420  limcvallem  21462  ellimc3  21470  cnlimci  21480  cnmptlimc  21481  dvferm1lem  21572  dvferm1  21573  dvferm2lem  21574  dvferm2  21575  dvlipcn  21582  dvle  21595  lhop1lem  21601  lhop1  21602  dvfsumge  21610  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumlem4  21617  dvfsum2  21622  ftc1a  21625  ftc1lem4  21627  itgsubstlem  21636  fta1glem2  21754  fta1g  21755  plyeq0lem  21794  dgrcolem2  21857  dgrco  21858  plydivlem4  21878  plydivex  21879  fta1lem  21889  fta1  21890  vieta1lem2  21893  vieta1  21894  aalioulem2  21915  aalioulem4  21917  tayl0  21943  ulmi  21967  ulmclm  21968  ulmshftlem  21970  ulmcaulem  21975  ulmcau  21976  ulmcn  21980  ulmdvlem1  21981  ulmdvlem3  21983  ulmdv  21984  pserulm  22003  efif1olem4  22117  rlimcnp  22475  rlimcnp2  22476  xrlimcnp  22478  cxploglim  22487  scvxcvx  22495  wilthlem2  22523  ftalem3  22528  fsumdvdscom  22641  musumsum  22648  chtub  22667  fsumvma  22668  perfectlem2  22685  dchrelbas3  22693  dchrelbasd  22694  dchrn0  22705  dchrptlem2  22720  lgsval2lem  22761  lgsdirnn0  22794  lgsdinn0  22795  2sqlem6  22824  2sqlem10  22829  dchrisumlema  22853  dchrisumlem1  22854  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusum2  22859  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrisum0flblem2  22874  dchrisum0flb  22875  dchrisum0lem1b  22880  dchrisum0lem2  22883  2vmadivsumlem  22905  chpdifbndlem1  22918  selberg3lem1  22922  selberg4lem1  22925  pntrsumbnd2  22932  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntpbnd1  22951  pntibndlem2  22956  pntibndlem3  22957  pntibnd  22958  pntlemn  22965  pntlemj  22968  pntlemi  22969  pntlemo  22972  pntlem3  22974  pntleml  22976  ostth2lem1  22983  ostth2lem2  22999  ostth3  23003  brbtwn2  23286  colinearalg  23291  axcontlem4  23348  nbgra0nb  23475  nbgrassovt  23481  cusgrarn  23502  usgrasscusgra  23526  isgrpo  23818  isgrp2d  23857  opidon  23944  exidu1  23948  rngoideu  24006  blocnilem  24339  ip2eqi  24392  ubthlem1  24406  minvecolem3  24412  htthlem  24454  hial0  24639  hial02  24640  hial2eq  24643  ocorth  24829  occllem  24841  pjhthlem1  24929  h1de2i  25091  pjjsi  25238  lnopunilem1  25549  lnophmlem1  25555  nmcexi  25565  riesz4i  25602  mdi  25834  mdbr3  25836  mdbr4  25837  dmdi  25841  dmdbr3  25844  dmdbr4  25845  dmdi4  25846  mdslmd1i  25868  atss  25885  atom1d  25892  atmd  25938  sumdmdlem2  25958  cdj1i  25972  cdj3i  25980  nn0min  26224  archiabllem1a  26342  archiabllem2a  26345  archiabl  26349  rngurd  26390  isarchiofld  26419  fmcncfil  26495  sigaclcu  26694  unelsiga  26711  measvun  26757  mbfmcnvima  26806  sibfima  26858  signstfvneq0  27107  lgamgulmlem5  27153  lgambdd  27157  lgamcvglem  27160  derangenlem  27193  subfacp1lem5  27206  subfacp1lem6  27207  rescon  27269  cvmcov  27286  cvmliftlem3  27310  cvmlift2lem10  27335  cvmliftphtlem  27340  ghomgrpilem1  27438  ghomf1olem  27447  clim2prod  27537  ntrivcvgfvn0  27548  fprodm1  27611  fprod1p  27612  fprodcom2  27629  dfon2lem6  27735  poseq  27848  soseq  27849  nocvxminlem  27965  nobndlem6  27972  fin2so  28554  mbfresfi  28576  ftc1cnnclem  28603  opnrebl2  28654  nn0prpwlem  28655  nn0prpw  28656  comppfsc  28717  neibastop2lem  28719  neibastop2  28720  filnetlem4  28740  seqpo  28781  incsequz  28782  mettrifi  28791  geomcau  28793  caushft  28795  sstotbnd2  28811  equivtotbnd  28815  totbndbnd  28826  ismtybndlem  28843  heibor1lem  28846  bfplem2  28860  isdrngo2  28902  unichnidl  28969  incssnn0  29185  lnmlssfg  29571  unxpwdom3  29586  fnchoice  29889  wwlknredwwlkn  30496  clwwlkf1  30596  clwwlkext2edg  30602  wwlkextproplem2  30699  3cyclfrgrarn1  30742  n4cyclfrgra  30748  frgrawopreglem4  30778  frgrawopreg1  30781  frgrawopreg2  30782  extwwlkfablem2  30809  lcosslsp  31079  linindslinci  31089  lindslinindsimp1  31098  ldepsnlinclem1  31154  ldepsnlinclem2  31155  lsat0cv  32984  lcvexchlem4  32988  lcvexchlem5  32989  eqlkr3  33052  lub0N  33140  glb0N  33144  cvrnbtwn  33222  ltrneq2  34098  trlval2  34113  lpolsatN  35439  lpolpolsatN  35440  hdmap14lem12  35833
  Copyright terms: Public domain W3C validator