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

Theorem rspcv 3008
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 1626 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3006 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721   A.wral 2666
This theorem is referenced by:  rspccv  3009  rspcva  3010  rspccva  3011  rspc3v  3021  rr19.3v  3037  rr19.28v  3038  rspsbc  3199  intmin  4030  somo  4497  fr2nr  4520  ralxfrALT  4701  fr3nr  4719  limuni3  4791  tfinds  4798  funcnvuni  5477  weniso  6034  knatar  6039  grprinvlem  6244  grprinvd  6245  caofref  6289  onnseq  6565  smo11  6585  tfrlem2  6596  tfrlem9  6605  tz7.49  6661  omeulem1  6784  oeordi  6789  nneneq  7249  frfi  7311  unblem2  7319  unbnn2  7323  xpfi  7337  ordiso2  7440  ordtypelem6  7448  ordtypelem7  7449  cantnflem1c  7599  cantnflem1  7601  rankunb  7732  tcrank  7764  carduni  7824  dfac8alem  7866  acni  7882  alephinit  7932  aceq3lem  7957  dfac5  7965  dfac12lem2  7980  dfac12r  7982  dfac12k  7983  pwsdompw  8040  cflm  8086  fin1ai  8129  fin2i  8131  isfin2-2  8155  fin23lem17  8174  fin23lem39  8186  isf32lem1  8189  isf32lem2  8190  isf34lem4  8213  hsmexlem4  8265  axcc3  8274  domtriomlem  8278  axdc3lem2  8287  axdc4lem  8291  axcclem  8293  ttukeylem5  8349  ttukeylem6  8350  axdclem  8355  alephval2  8403  canth4  8478  pwfseqlem5  8494  winainflem  8524  wununi  8537  wunpw  8538  eltskm  8674  squeeze0  9869  lbreu  9914  nnsub  9994  ublbneg  10516  zsupss  10521  uzwo3  10525  zmax  10527  zbtwnre  10528  xrub  10846  fzrevral  11086  axdc4uzlem  11276  seqcl2  11296  seqcl  11298  seqf  11299  seqfveq2  11300  seqfveq  11302  seqshft2  11304  monoord  11308  monoord2  11309  sermono  11310  seqsplit  11311  seqcaopr3  11313  seqid  11323  seqid2  11324  seqhomo  11325  seqz  11326  discr1  11470  discr  11471  faclbnd4lem4  11542  hashbclem  11656  wrdind  11746  recan  12095  cau3lem  12113  caubnd2  12116  limsupgre  12230  climi  12259  rlimi  12262  rlimclim1  12294  rlimclim  12295  climrlim2  12296  climshftlem  12323  rlimcld2  12327  rlimcn1  12337  climcn1  12340  subcn2  12343  isercoll  12416  isercoll2  12417  climcau  12419  caucvgrlem  12421  caucvgb  12428  serf0  12429  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  fsumm1  12492  fsum1p  12494  fsumcom2  12513  fsumge1  12531  fsumtscopo  12536  fsumtscopo2  12537  fsumparts  12540  o1fsum  12547  isum1p  12576  isumnn0nn  12577  isumrpcl  12578  climcndslem1  12584  climcndslem2  12585  climcnds  12586  cvgrat  12615  mertenslem1  12616  mertens  12618  sqr2irr  12803  ndvdssub  12882  prmind2  13045  nprm  13048  dvdsprm  13054  coprm  13055  pcmpt  13216  pcmpt2  13217  pcmptdvds  13218  pcfac  13223  prmpwdvds  13227  unbenlem  13231  prmreclem4  13242  prmreclem5  13243  vdwlem1  13304  vdwlem2  13305  vdwlem9  13312  vdwlem10  13313  vdwlem13  13316  vdwnnlem1  13318  rami  13338  ramcl  13352  catidex  13854  catideu  13855  iscatd2  13861  catlid  13863  catrid  13864  subcidcl  13996  funcid  14022  yonedalem4c  14329  yonffthlem  14334  isdrs2  14351  lubid  14394  lubun  14505  poslubmo  14528  spwmo  14613  grpidd2  14797  mulgsubcl  14859  issubg4  14916  ghmf1  14989  fislw  15214  efgi  15306  efgi2  15312  efgsdmi  15319  efgsrel  15321  gexexlem  15422  gsumzaddlem  15481  gsummhm2  15490  dprdcntz  15521  dprddisj  15522  dprdss  15542  dprd2dlem2  15553  dprd2da  15555  dpjrid  15575  ablfac1eu  15586  pgpfac1lem1  15587  pgpfaclem2  15595  issrngd  15904  islmodd  15911  islmhm2  16069  islbs2  16181  lbsextlem4  16188  rrgeq0i  16304  mvrf1  16444  mplsubglem  16453  mpllsslem  16454  subrgasclcl  16514  prmirredlem  16728  ip2eq  16839  isclo2  17107  lmcvg  17280  cnpnei  17282  iscncl  17287  cncls  17292  lmss  17316  lmff  17319  cnt0  17364  isnrm2  17376  cnrmi  17378  isreg2  17395  cmpcov  17406  tgcmp  17418  uncmp  17420  fiuncmp  17421  dfcon2  17435  1stcclb  17460  1stcfb  17461  2ndcctbss  17471  1stcelcls  17477  restnlly  17498  islly2  17500  lly1stc  17512  kgeni  17522  kgencn2  17542  ptpjpre1  17556  ptbasfi  17566  ptpjopn  17597  dfac14  17603  txtube  17625  txlm  17633  cnmpt11  17648  cnmpt21  17656  cnmptkp  17665  cnmptk1p  17670  qtopomap  17703  qtopcmap  17704  kqfvima  17715  kqt0lem  17721  isr0  17722  nrmr0reg  17734  fgss2  17859  isufil2  17893  cfinufil  17913  flimopn  17960  fbflim2  17962  flimcf  17967  flfneii  17977  cnpflf  17986  fclssscls  18003  fclsnei  18004  fclsrest  18009  fclscf  18010  flimfnfcls  18013  fclscmp  18015  isfcf  18019  fcfnei  18020  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem3  18038  tgpt0  18101  tsmsi  18116  tsmsgsum  18121  tsmsres  18126  tsmsxplem1  18135  tsmsxplem2  18136  tsmsxp  18137  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  isucn2  18262  ucnima  18264  ucncn  18268  cfiluexsm  18273  psmet0  18292  imasdsf1olem  18356  prdsbl  18474  metss  18491  comet  18496  metcnp3  18523  isngp4  18611  nmoi  18715  mulc1cncf  18888  cncfco  18890  cnheiborlem  18932  cnheibor  18933  bndth  18936  lebnumii  18944  nmoleub2lem2  19077  nmoleub3  19080  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  lmmcvg  19167  iscfil3  19179  iscau2  19183  iscau4  19185  cmetcaulem  19194  iscmet3lem1  19197  iscmet3lem2  19198  equivcfil  19205  equivcau  19206  lmcau  19218  pjthlem1  19291  pjthlem2  19292  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ivth2  19305  ivthle  19306  ivthle2  19307  ivthicc  19308  ovoliunlem1  19351  ovolshftlem1  19358  ovolscalem1  19362  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2  19371  volsup  19403  dyadmbl  19445  vitalilem2  19454  vitalilem3  19455  mbfdm  19473  ismbf  19475  ismbf3d  19499  cncombf  19503  itg2seq  19587  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  iblitg  19613  itgconst  19663  itgfsum  19671  limcvallem  19711  ellimc3  19719  cnlimci  19729  cnmptlimc  19730  dvferm1lem  19821  dvferm1  19822  dvferm2lem  19823  dvferm2  19824  dvlipcn  19831  dvle  19844  lhop1lem  19850  lhop1  19851  dvfsumge  19859  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  itgsubstlem  19885  fta1glem2  20042  fta1g  20043  plyeq0lem  20082  dgrcolem2  20145  dgrco  20146  plydivlem4  20166  plydivex  20167  fta1lem  20177  fta1  20178  vieta1lem2  20181  vieta1  20182  aalioulem2  20203  aalioulem4  20205  tayl0  20231  ulmi  20255  ulmclm  20256  ulmshftlem  20258  ulmcaulem  20263  ulmcau  20264  ulmcn  20268  ulmdvlem1  20269  ulmdvlem3  20271  ulmdv  20272  pserulm  20291  efif1olem4  20400  rlimcnp  20757  rlimcnp2  20758  xrlimcnp  20760  cxploglim  20769  scvxcvx  20777  wilthlem2  20805  ftalem3  20810  fsumdvdscom  20923  musumsum  20930  chtub  20949  fsumvma  20950  perfectlem2  20967  dchrelbas3  20975  dchrelbasd  20976  dchrn0  20987  dchrptlem2  21002  lgsval2lem  21043  lgsdirnn0  21076  lgsdinn0  21077  2sqlem6  21106  2sqlem10  21111  dchrisumlema  21135  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0flb  21157  dchrisum0lem1b  21162  dchrisum0lem2  21165  2vmadivsumlem  21187  chpdifbndlem1  21200  selberg3lem1  21204  selberg4lem1  21207  pntrsumbnd2  21214  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd1  21233  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemn  21247  pntlemj  21250  pntlemi  21251  pntlemo  21254  pntlem3  21256  pntleml  21258  ostth2lem1  21265  ostth2lem2  21281  ostth3  21285  nbgra0nb  21394  nbgrassovt  21400  cusgrarn  21421  usgrasscusgra  21445  isgrpo  21737  isgrp2d  21776  opidon  21863  exidu1  21867  rngoideu  21925  blocnilem  22258  ip2eqi  22311  ubthlem1  22325  minvecolem3  22331  htthlem  22373  hial0  22557  hial02  22558  hial2eq  22561  ocorth  22746  occllem  22758  pjhthlem1  22846  h1de2i  23008  pjjsi  23155  lnopunilem1  23466  lnophmlem1  23472  nmcexi  23482  riesz4i  23519  mdi  23751  mdbr3  23753  mdbr4  23754  dmdi  23758  dmdbr3  23761  dmdbr4  23762  dmdi4  23763  mdslmd1i  23785  atss  23802  atom1d  23809  atmd  23855  sumdmdlem2  23875  cdj1i  23889  cdj3i  23897  ofldadd  24191  ofldmul  24192  fmcncfil  24270  sigaclcu  24453  unelsiga  24470  measvun  24516  mbfmcnvima  24560  sibfima  24606  lgamgulmlem5  24770  lgambdd  24774  lgamcvglem  24777  derangenlem  24810  subfacp1lem5  24823  subfacp1lem6  24824  rescon  24886  cvmcov  24903  cvmliftlem3  24927  cvmlift2lem10  24952  cvmliftphtlem  24957  ghomgrpilem1  25049  ghomf1olem  25058  dedekind  25140  clim2prod  25169  ntrivcvgfvn0  25180  fprodm1  25243  fprod1p  25244  fprodcom2  25261  dfon2lem6  25358  poseq  25467  soseq  25468  nocvxminlem  25558  nobndlem6  25565  brbtwn2  25748  colinearalg  25753  axcontlem4  25810  mbfresfi  26152  ftc1cnnclem  26177  opnrebl2  26214  nn0prpwlem  26215  nn0prpw  26216  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  filnetlem4  26300  seqpo  26341  incsequz  26342  mettrifi  26353  geomcau  26355  caushft  26357  sstotbnd2  26373  equivtotbnd  26377  totbndbnd  26388  ismtybndlem  26405  heibor1lem  26408  bfplem2  26422  isdrngo2  26464  unichnidl  26531  incssnn0  26655  lnmlssfg  27046  unxpwdom3  27124  fnchoice  27567  3cyclfrgrarn1  28116  n4cyclfrgra  28122  frgrawopreglem4  28150  frgrawopreg1  28153  frgrawopreg2  28154  lubunNEW  29456  lsat0cv  29516  lcvexchlem4  29520  lcvexchlem5  29521  eqlkr3  29584  lub0N  29672  glb0N  29676  cvrnbtwn  29754  ltrneq2  30630  trlval2  30645  lpolsatN  31971  lpolpolsatN  31972  hdmap14lem12  32365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918
  Copyright terms: Public domain W3C validator