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

Theorem rspcv 2956
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 1619 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 2954 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642    e. wcel 1710   A.wral 2619
This theorem is referenced by:  rspccv  2957  rspcva  2958  rspccva  2959  rspc3v  2969  rr19.3v  2985  rr19.28v  2986  rspsbc  3145  intmin  3963  somo  4430  fr2nr  4453  ralxfrALT  4635  fr3nr  4653  limuni3  4725  tfinds  4732  funcnvuni  5399  weniso  5939  knatar  5944  grprinvlem  6145  grprinvd  6146  caofref  6190  onnseq  6448  smo11  6468  tfrlem2  6479  tfrlem9  6488  tz7.49  6544  omeulem1  6667  oeordi  6672  nneneq  7132  frfi  7192  unblem2  7200  unbnn2  7204  xpfi  7218  ordiso2  7320  ordtypelem6  7328  ordtypelem7  7329  cantnflem1c  7479  cantnflem1  7481  rankunb  7612  tcrank  7644  carduni  7704  dfac8alem  7746  acni  7762  alephinit  7812  aceq3lem  7837  dfac5  7845  dfac12lem2  7860  dfac12r  7862  dfac12k  7863  pwsdompw  7920  cflm  7966  fin1ai  8009  fin2i  8011  isfin2-2  8035  fin23lem17  8054  fin23lem39  8066  isf32lem1  8069  isf32lem2  8070  isf34lem4  8093  hsmexlem4  8145  axcc3  8154  domtriomlem  8158  axdc3lem2  8167  axdc4lem  8171  axcclem  8173  ttukeylem5  8230  ttukeylem6  8231  axdclem  8236  alephval2  8284  canth4  8359  pwfseqlem5  8375  winainflem  8405  wununi  8418  wunpw  8419  eltskm  8555  squeeze0  9749  lbreu  9794  nnsub  9874  ublbneg  10394  zsupss  10399  uzwo3  10403  zmax  10405  zbtwnre  10406  xrub  10722  fzrevral  10958  axdc4uzlem  11136  seqcl2  11156  seqcl  11158  seqf  11159  seqfveq2  11160  seqfveq  11162  seqshft2  11164  monoord  11168  monoord2  11169  sermono  11170  seqsplit  11171  seqcaopr3  11173  seqid  11183  seqid2  11184  seqhomo  11185  seqz  11186  discr1  11330  discr  11331  faclbnd4lem4  11402  hashbclem  11486  wrdind  11573  recan  11916  cau3lem  11934  caubnd2  11937  limsupgre  12051  climi  12080  rlimi  12083  rlimclim1  12115  rlimclim  12116  climrlim2  12117  climshftlem  12144  rlimcld2  12148  rlimcn1  12158  climcn1  12161  subcn2  12164  isercoll  12237  isercoll2  12238  climcau  12240  caucvgrlem  12242  caucvgb  12249  serf0  12250  iseraltlem2  12252  iseraltlem3  12253  iseralt  12254  fsumm1  12313  fsum1p  12315  fsumcom2  12334  fsumge1  12352  fsumtscopo  12357  fsumtscopo2  12358  fsumparts  12361  o1fsum  12368  isum1p  12397  isumnn0nn  12398  isumrpcl  12399  climcndslem1  12405  climcndslem2  12406  climcnds  12407  cvgrat  12436  mertenslem1  12437  mertens  12439  sqr2irr  12624  ndvdssub  12703  prmind2  12866  nprm  12869  dvdsprm  12875  coprm  12876  pcmpt  13037  pcmpt2  13038  pcmptdvds  13039  pcfac  13044  prmpwdvds  13048  unbenlem  13052  prmreclem4  13063  prmreclem5  13064  vdwlem1  13125  vdwlem2  13126  vdwlem9  13133  vdwlem10  13134  vdwlem13  13137  vdwnnlem1  13139  rami  13159  ramcl  13173  catidex  13675  catideu  13676  iscatd2  13682  catlid  13684  catrid  13685  subcidcl  13817  funcid  13843  yonedalem4c  14150  yonffthlem  14155  isdrs2  14172  lubid  14215  lubun  14326  poslubmo  14349  spwmo  14434  grpidd2  14618  mulgsubcl  14680  issubg4  14737  ghmf1  14810  fislw  15035  efgi  15127  efgi2  15133  efgsdmi  15140  efgsrel  15142  gexexlem  15243  gsumzaddlem  15302  gsummhm2  15311  dprdcntz  15342  dprddisj  15343  dprdss  15363  dprd2dlem2  15374  dprd2da  15376  dpjrid  15396  ablfac1eu  15407  pgpfac1lem1  15408  pgpfaclem2  15416  issrngd  15725  islmodd  15732  islmhm2  15894  islbs2  16006  lbsextlem4  16013  rrgeq0i  16129  mvrf1  16269  mplsubglem  16278  mpllsslem  16279  subrgasclcl  16339  prmirredlem  16552  ip2eq  16663  isclo2  16931  lmcvg  17098  cnpnei  17099  iscncl  17104  cncls  17109  lmss  17132  lmff  17135  cnt0  17180  isnrm2  17192  cnrmi  17194  isreg2  17211  cmpcov  17222  tgcmp  17234  uncmp  17236  fiuncmp  17237  dfcon2  17251  1stcclb  17276  1stcfb  17277  2ndcctbss  17287  1stcelcls  17293  restnlly  17314  islly2  17316  lly1stc  17328  kgeni  17338  kgencn2  17358  ptpjpre1  17372  ptbasfi  17382  ptpjopn  17412  dfac14  17418  txtube  17440  txlm  17448  cnmpt11  17463  cnmpt21  17471  cnmptkp  17480  cnmptk1p  17485  qtopomap  17515  qtopcmap  17516  kqfvima  17527  kqt0lem  17533  isr0  17534  nrmr0reg  17546  fgss2  17671  isufil2  17705  cfinufil  17725  flimopn  17772  fbflim2  17774  flimcf  17779  flfneii  17789  cnpflf  17798  fclssscls  17815  fclsnei  17816  fclsrest  17821  fclscf  17822  flimfnfcls  17825  fclscmp  17827  isfcf  17831  fcfnei  17832  alexsubALTlem3  17845  alexsubALTlem4  17846  alexsubALT  17847  ptcmplem3  17850  tgpt0  17903  tsmsi  17918  tsmsgsum  17923  tsmsres  17928  tsmsxplem1  17937  tsmsxplem2  17938  tsmsxp  17939  imasdsf1olem  18039  prdsbl  18139  metss  18156  comet  18161  metcnp3  18188  isngp4  18235  nmoi  18339  mulc1cncf  18512  cncfco  18514  cnheiborlem  18556  cnheibor  18557  bndth  18560  lebnumii  18568  nmoleub2lem2  18701  nmoleub3  18704  ipcau2  18768  tchcphlem1  18769  tchcphlem2  18770  lmmcvg  18791  iscfil3  18803  iscau2  18807  iscau4  18809  cmetcaulem  18818  iscmet3lem1  18821  iscmet3lem2  18822  equivcfil  18829  equivcau  18830  lmcau  18842  pjthlem1  18905  pjthlem2  18906  ivthlem1  18915  ivthlem2  18916  ivthlem3  18917  ivth2  18919  ivthle  18920  ivthle2  18921  ivthicc  18922  ovoliunlem1  18965  ovolshftlem1  18972  ovolscalem1  18976  ovolicc2lem3  18982  ovolicc2lem4  18983  ovolicc2  18985  volsup  19017  dyadmbl  19059  vitalilem2  19068  vitalilem3  19069  mbfdm  19087  ismbf  19089  ismbf3d  19113  cncombf  19117  itg2seq  19201  itg2monolem2  19210  itg2monolem3  19211  itg2mono  19212  iblitg  19227  itgconst  19277  itgfsum  19285  limcvallem  19325  ellimc3  19333  cnlimci  19343  cnmptlimc  19344  dvferm1lem  19435  dvferm1  19436  dvferm2lem  19437  dvferm2  19438  dvlipcn  19445  dvle  19458  lhop1lem  19464  lhop1  19465  dvfsumge  19473  dvfsumlem2  19478  dvfsumlem3  19479  dvfsumlem4  19480  dvfsum2  19485  ftc1a  19488  ftc1lem4  19490  itgsubstlem  19499  fta1glem2  19656  fta1g  19657  plyeq0lem  19696  dgrcolem2  19759  dgrco  19760  plydivlem4  19780  plydivex  19781  fta1lem  19791  fta1  19792  vieta1lem2  19795  vieta1  19796  aalioulem2  19817  aalioulem4  19819  tayl0  19845  ulmi  19869  ulmclm  19870  ulmshftlem  19872  ulmcaulem  19877  ulmcau  19878  ulmcn  19882  ulmdvlem1  19883  ulmdvlem3  19885  ulmdv  19886  pserulm  19905  efif1olem4  20014  rlimcnp  20371  rlimcnp2  20372  xrlimcnp  20374  cxploglim  20383  scvxcvx  20391  wilthlem2  20419  ftalem3  20424  fsumdvdscom  20537  musumsum  20544  chtub  20563  fsumvma  20564  perfectlem2  20581  dchrelbas3  20589  dchrelbasd  20590  dchrn0  20601  dchrptlem2  20616  lgsval2lem  20657  lgsdirnn0  20690  lgsdinn0  20691  2sqlem6  20720  2sqlem10  20725  dchrisumlema  20749  dchrisumlem1  20750  dchrisumlem2  20751  dchrisumlem3  20752  dchrmusum2  20755  dchrvmasumlem2  20759  dchrvmasumlem3  20760  dchrvmasumiflem1  20762  dchrisum0flblem2  20770  dchrisum0flb  20771  dchrisum0lem1b  20776  dchrisum0lem2  20779  2vmadivsumlem  20801  chpdifbndlem1  20814  selberg3lem1  20818  selberg4lem1  20821  pntrsumbnd2  20828  pntrlog2bndlem2  20839  pntrlog2bndlem3  20840  pntrlog2bndlem5  20842  pntrlog2bndlem6  20844  pntpbnd1  20847  pntibndlem2  20852  pntibndlem3  20853  pntibnd  20854  pntlemn  20861  pntlemj  20864  pntlemi  20865  pntlemo  20868  pntlem3  20870  pntleml  20872  ostth2lem1  20879  ostth2lem2  20895  ostth3  20899  isgrpo  20975  isgrp2d  21014  opidon  21101  exidu1  21105  rngoideu  21163  blocnilem  21496  ip2eqi  21549  ubthlem1  21563  minvecolem3  21569  htthlem  21611  hial0  21795  hial02  21796  hial2eq  21799  ocorth  21984  occllem  21996  pjhthlem1  22084  h1de2i  22246  pjjsi  22393  lnopunilem1  22704  lnophmlem1  22710  nmcexi  22720  riesz4i  22757  mdi  22989  mdbr3  22991  mdbr4  22992  dmdi  22996  dmdbr3  22999  dmdbr4  23000  dmdi4  23001  mdslmd1i  23023  atss  23040  atom1d  23047  atmd  23093  sumdmdlem2  23113  cdj1i  23127  cdj3i  23135  fmcncfil  23473  ustincl  23513  ustdiag  23514  ustinvel  23515  ustexhalf  23516  ucnima  23576  cfiluexsm  23584  sigaclcu  23766  unelsiga  23783  measvun  23827  mbfmcnvima  23871  dya2icoseg2  23892  lgamgulmlem5  24066  lgambdd  24070  lgamcvglem  24073  derangenlem  24106  subfacp1lem5  24119  subfacp1lem6  24120  rescon  24181  cvmcov  24198  cvmliftlem3  24222  cvmlift2lem10  24247  cvmliftphtlem  24252  ghomgrpilem1  24396  ghomf1olem  24405  dedekind  24488  clim2prod  24517  ntrivcvgfvn0  24528  fprodm1  24591  fprod1p  24592  dfon2lem6  24702  poseq  24811  soseq  24812  nocvxminlem  24902  nobndlem6  24909  brbtwn2  25092  colinearalg  25097  axcontlem4  25154  ftc1cnnclem  25513  opnrebl2  25560  nn0prpwlem  25562  nn0prpw  25563  comppfsc  25631  neibastop2lem  25633  neibastop2  25634  filnetlem4  25654  seqpo  25781  incsequz  25782  mettrifi  25797  geomcau  25799  caushft  25801  sstotbnd2  25821  equivtotbnd  25825  totbndbnd  25836  ismtybndlem  25853  heibor1lem  25856  bfplem2  25870  isdrngo2  25912  unichnidl  25979  incssnn0  26109  lnmlssfg  26501  unxpwdom3  26579  fnchoice  27023  nbgra0nb  27595  nbgrassovt  27601  cusgrarn  27622  usgrasscusgra  27646  3cyclfrgrarn1  27845  n4cyclfrgra  27851  frgrawopreglem4  27880  frgrawopreg1  27883  frgrawopreg2  27884  lubunNEW  29232  lsat0cv  29292  lcvexchlem4  29296  lcvexchlem5  29297  eqlkr3  29360  lub0N  29448  glb0N  29452  cvrnbtwn  29530  ltrneq2  30406  trlval2  30421  lpolsatN  31747  lpolpolsatN  31748  hdmap14lem12  32141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-v 2866
  Copyright terms: Public domain W3C validator