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

Theorem rspcv 3064
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 1673 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3062 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756   A.wral 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-v 2969
This theorem is referenced by:  rspccv  3065  rspcva  3066  rspccva  3067  rspc3v  3077  rr19.3v  3096  rr19.28v  3097  rspsbc  3271  intmin  4143  ralxfrALT  4506  somo  4670  fr2nr  4693  nvocnv  5983  weniso  6040  knatar  6043  grprinvlem  6296  grprinvd  6297  caofref  6341  fr3nr  6386  limuni3  6458  tfinds  6465  funcnvuni  6525  onnseq  6797  smo11  6817  tfrlem1  6827  tfrlem5  6831  tfrlem9  6836  tz7.49  6892  omeulem1  7013  oeordi  7018  nneneq  7486  frfi  7549  unblem2  7557  unbnn2  7561  xpfi  7575  ordiso2  7721  ordtypelem6  7729  ordtypelem7  7730  cantnflem1c  7887  cantnflem1  7889  cantnflem1cOLD  7910  cantnflem1OLD  7912  rankunb  8049  tcrank  8083  carduni  8143  dfac8alem  8191  acni  8207  alephinit  8257  aceq3lem  8282  dfac5  8290  dfac12lem2  8305  dfac12r  8307  dfac12k  8308  pwsdompw  8365  cflm  8411  fin1ai  8454  fin2i  8456  isfin2-2  8480  fin23lem17  8499  fin23lem39  8511  isf32lem1  8514  isf32lem2  8515  isf34lem4  8538  hsmexlem4  8590  axcc3  8599  domtriomlem  8603  axdc3lem2  8612  axdc4lem  8616  axcclem  8618  ttukeylem5  8674  ttukeylem6  8675  axdclem  8680  alephval2  8728  canth4  8806  pwfseqlem5  8822  winainflem  8852  wununi  8865  wunpw  8866  eltskm  9002  dedekind  9525  squeeze0  10227  lbreu  10272  nnsub  10352  ublbneg  10931  zsupss  10936  uzwo3  10940  zmax  10942  zbtwnre  10943  xrub  11266  fzrevral  11536  axdc4uzlem  11796  seqcl2  11816  seqcl  11818  seqf  11819  seqfveq2  11820  seqfveq  11822  seqshft2  11824  monoord  11828  monoord2  11829  sermono  11830  seqsplit  11831  seqcaopr3  11833  seqid  11843  seqid2  11844  seqhomo  11845  seqz  11846  discr1  11992  discr  11993  faclbnd4lem4  12064  hashbclem  12197  wrdind  12363  wrd2ind  12364  recan  12816  cau3lem  12834  caubnd2  12837  limsupgre  12951  climi  12980  rlimi  12983  rlimclim1  13015  rlimclim  13016  climrlim2  13017  climshftlem  13044  rlimcld2  13048  rlimcn1  13058  climcn1  13061  subcn2  13064  isercoll  13137  isercoll2  13138  climcau  13140  caucvgrlem  13142  caucvgb  13149  serf0  13150  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  fsumm1  13212  fsum1p  13214  fsumcom2  13233  fsumge1  13252  fsumtscopo  13257  fsumtscopo2  13258  fsumparts  13261  o1fsum  13268  isum1p  13296  isumnn0nn  13297  isumrpcl  13298  climcndslem1  13304  climcndslem2  13305  climcnds  13306  cvgrat  13335  mertenslem1  13336  mertens  13338  sqr2irr  13523  ndvdssub  13603  prmind2  13766  nprm  13769  dvdsprm  13777  coprm  13778  pcmpt  13946  pcmpt2  13947  pcmptdvds  13948  pcfac  13953  prmpwdvds  13957  unbenlem  13961  prmreclem4  13972  prmreclem5  13973  vdwlem1  14034  vdwlem2  14035  vdwlem9  14042  vdwlem10  14043  vdwlem13  14046  vdwnnlem1  14048  rami  14068  ramcl  14082  catidex  14604  catideu  14605  iscatd2  14611  catlid  14613  catrid  14614  subcidcl  14746  funcid  14772  yonedalem4c  15079  yonffthlem  15084  isdrs2  15101  lublecllem  15150  lubun  15285  poslubmo  15308  posglbmo  15309  grpidd2  15566  mulgsubcl  15632  issubg4  15691  ghmf1  15766  fislw  16115  efgi  16207  efgi2  16213  efgsdmi  16220  efgsrel  16222  gexexlem  16325  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsummhm2  16424  gsummhm2OLD  16425  dprdcntz  16480  dprddisj  16481  dprdss  16514  dprd2dlem2  16527  dprd2da  16529  dpjrid  16549  ablfac1eu  16562  pgpfac1lem1  16563  pgpfaclem2  16571  srgrz  16615  srglz  16616  srgisid  16617  issrngd  16924  islmodd  16932  islmhm2  17096  islbs2  17212  lbsextlem4  17219  rrgeq0i  17337  mvrf1  17475  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  subrgasclcl  17556  prmirredlem  17892  prmirredlemOLD  17895  ip2eq  18057  frlmphl  18181  mdetralt  18389  isclo2  18667  lmcvg  18841  cnpnei  18843  iscncl  18848  cncls  18853  lmss  18877  lmff  18880  cnt0  18925  isnrm2  18937  cnrmi  18939  isreg2  18956  cmpcov  18967  tgcmp  18979  uncmp  18981  fiuncmp  18982  bwthOLD  18989  dfcon2  18998  1stcclb  19023  1stcfb  19024  2ndcctbss  19034  1stcelcls  19040  restnlly  19061  islly2  19063  lly1stc  19075  kgeni  19085  kgencn2  19105  ptpjpre1  19119  ptbasfi  19129  ptpjopn  19160  dfac14  19166  txtube  19188  txlm  19196  cnmpt11  19211  cnmpt21  19219  cnmptkp  19228  cnmptk1p  19233  qtopomap  19266  qtopcmap  19267  kqfvima  19278  kqt0lem  19284  isr0  19285  nrmr0reg  19297  fgss2  19422  isufil2  19456  cfinufil  19476  flimopn  19523  fbflim2  19525  flimcf  19530  flfneii  19540  cnpflf  19549  fclssscls  19566  fclsnei  19567  fclsrest  19572  fclscf  19573  flimfnfcls  19576  fclscmp  19578  isfcf  19582  fcfnei  19583  alexsubALTlem3  19596  alexsubALTlem4  19597  alexsubALT  19598  ptcmplem3  19601  tgpt0  19664  tsmsi  19679  tsmsgsum  19684  tsmsgsumOLD  19687  tsmsresOLD  19692  tsmsres  19693  tsmsxplem1  19702  tsmsxplem2  19703  tsmsxp  19704  ustincl  19757  ustdiag  19758  ustinvel  19759  ustexhalf  19760  isucn2  19829  ucnima  19831  ucncn  19835  cfiluexsm  19840  psmet0  19859  imasdsf1olem  19923  prdsbl  20041  metss  20058  comet  20063  metcnp3  20090  isngp4  20178  nmoi  20282  mulc1cncf  20456  cncfco  20458  cnheiborlem  20501  cnheibor  20502  bndth  20505  lebnumii  20513  nmoleub2lem2  20646  nmoleub3  20649  ipcau2  20724  tchcphlem1  20725  tchcphlem2  20726  lmmcvg  20747  iscfil3  20759  iscau2  20763  iscau4  20765  cmetcaulem  20774  iscmet3lem1  20777  iscmet3lem2  20778  equivcfil  20785  equivcau  20786  lmcau  20798  pjthlem1  20899  pjthlem2  20900  ivthlem1  20910  ivthlem2  20911  ivthlem3  20912  ivth2  20914  ivthle  20915  ivthle2  20916  ivthicc  20917  ovoliunlem1  20960  ovolshftlem1  20967  ovolscalem1  20971  ovolicc2lem3  20977  ovolicc2lem4  20978  ovolicc2  20980  volsup  21012  dyadmbl  21055  vitalilem2  21064  vitalilem3  21065  mbfdm  21081  ismbf  21083  ismbf3d  21107  cncombf  21111  itg2seq  21195  itg2monolem2  21204  itg2monolem3  21205  itg2mono  21206  iblitg  21221  itgconst  21271  itgfsum  21279  limcvallem  21321  ellimc3  21329  cnlimci  21339  cnmptlimc  21340  dvferm1lem  21431  dvferm1  21432  dvferm2lem  21433  dvferm2  21434  dvlipcn  21441  dvle  21454  lhop1lem  21460  lhop1  21461  dvfsumge  21469  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumlem4  21476  dvfsum2  21481  ftc1a  21484  ftc1lem4  21486  itgsubstlem  21495  fta1glem2  21613  fta1g  21614  plyeq0lem  21653  dgrcolem2  21716  dgrco  21717  plydivlem4  21737  plydivex  21738  fta1lem  21748  fta1  21749  vieta1lem2  21752  vieta1  21753  aalioulem2  21774  aalioulem4  21776  tayl0  21802  ulmi  21826  ulmclm  21827  ulmshftlem  21829  ulmcaulem  21834  ulmcau  21835  ulmcn  21839  ulmdvlem1  21840  ulmdvlem3  21842  ulmdv  21843  pserulm  21862  efif1olem4  21976  rlimcnp  22334  rlimcnp2  22335  xrlimcnp  22337  cxploglim  22346  scvxcvx  22354  wilthlem2  22382  ftalem3  22387  fsumdvdscom  22500  musumsum  22507  chtub  22526  fsumvma  22527  perfectlem2  22544  dchrelbas3  22552  dchrelbasd  22553  dchrn0  22564  dchrptlem2  22579  lgsval2lem  22620  lgsdirnn0  22653  lgsdinn0  22654  2sqlem6  22683  2sqlem10  22688  dchrisumlema  22712  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumlem3  22723  dchrvmasumiflem1  22725  dchrisum0flblem2  22733  dchrisum0flb  22734  dchrisum0lem1b  22739  dchrisum0lem2  22742  2vmadivsumlem  22764  chpdifbndlem1  22777  selberg3lem1  22781  selberg4lem1  22784  pntrsumbnd2  22791  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntpbnd1  22810  pntibndlem2  22815  pntibndlem3  22816  pntibnd  22817  pntlemn  22824  pntlemj  22827  pntlemi  22828  pntlemo  22831  pntlem3  22833  pntleml  22835  ostth2lem1  22842  ostth2lem2  22858  ostth3  22862  brbtwn2  23102  colinearalg  23107  axcontlem4  23164  nbgra0nb  23291  nbgrassovt  23297  cusgrarn  23318  usgrasscusgra  23342  isgrpo  23634  isgrp2d  23673  opidon  23760  exidu1  23764  rngoideu  23822  blocnilem  24155  ip2eqi  24208  ubthlem1  24222  minvecolem3  24228  htthlem  24270  hial0  24455  hial02  24456  hial2eq  24459  ocorth  24645  occllem  24657  pjhthlem1  24745  h1de2i  24907  pjjsi  25054  lnopunilem1  25365  lnophmlem1  25371  nmcexi  25381  riesz4i  25418  mdi  25650  mdbr3  25652  mdbr4  25653  dmdi  25657  dmdbr3  25660  dmdbr4  25661  dmdi4  25662  mdslmd1i  25684  atss  25701  atom1d  25708  atmd  25754  sumdmdlem2  25774  cdj1i  25788  cdj3i  25796  nn0min  26041  archiabllem1a  26159  archiabllem2a  26162  archiabl  26166  rngurd  26207  isarchiofld  26236  fmcncfil  26313  sigaclcu  26512  unelsiga  26529  measvun  26575  mbfmcnvima  26624  sibfima  26676  signstfvneq0  26925  lgamgulmlem5  26971  lgambdd  26975  lgamcvglem  26978  derangenlem  27011  subfacp1lem5  27024  subfacp1lem6  27025  rescon  27087  cvmcov  27104  cvmliftlem3  27128  cvmlift2lem10  27153  cvmliftphtlem  27158  ghomgrpilem1  27255  ghomf1olem  27264  clim2prod  27354  ntrivcvgfvn0  27365  fprodm1  27428  fprod1p  27429  fprodcom2  27446  dfon2lem6  27552  poseq  27665  soseq  27666  nocvxminlem  27782  nobndlem6  27789  fin2so  28369  mbfresfi  28391  ftc1cnnclem  28418  opnrebl2  28469  nn0prpwlem  28470  nn0prpw  28471  comppfsc  28532  neibastop2lem  28534  neibastop2  28535  filnetlem4  28555  seqpo  28596  incsequz  28597  mettrifi  28606  geomcau  28608  caushft  28610  sstotbnd2  28626  equivtotbnd  28630  totbndbnd  28641  ismtybndlem  28658  heibor1lem  28661  bfplem2  28675  isdrngo2  28717  unichnidl  28784  incssnn0  29000  lnmlssfg  29386  unxpwdom3  29401  fnchoice  29704  wwlknredwwlkn  30311  clwwlkf1  30411  clwwlkext2edg  30417  wwlkextproplem2  30514  3cyclfrgrarn1  30557  n4cyclfrgra  30563  frgrawopreglem4  30593  frgrawopreg1  30596  frgrawopreg2  30597  extwwlkfablem2  30624  lcosslsp  30861  linindslinci  30871  lindslinindsimp1  30880  ldepsnlinclem1  30936  ldepsnlinclem2  30937  lsat0cv  32518  lcvexchlem4  32522  lcvexchlem5  32523  eqlkr3  32586  lub0N  32674  glb0N  32678  cvrnbtwn  32756  ltrneq2  33632  trlval2  33647  lpolsatN  34973  lpolpolsatN  34974  hdmap14lem12  35367
  Copyright terms: Public domain W3C validator