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

Theorem rspcv 3158
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 1772 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3156 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-v 3059
This theorem is referenced by:  rspccv  3159  rspcva  3160  rspccva  3161  rspc3v  3174  rr19.3v  3192  rr19.28v  3193  rspsbc  3358  intmin  4268  ralxfrALT  4633  somo  4808  fr2nr  4831  nvocnv  6205  weniso  6270  knatar  6273  grprinvlem  6534  grprinvd  6535  caofref  6584  fr3nr  6633  limuni3  6706  tfinds  6713  funcnvuni  6773  suppfnss  6967  onnseq  7089  smo11  7109  tfrlem1  7120  tfrlem5  7124  tfrlem9  7129  tz7.49  7188  omeulem1  7309  oeordi  7314  nneneq  7781  frfi  7842  unblem2  7850  unbnn2  7854  xpfi  7868  ordiso2  8056  ordtypelem6  8064  ordtypelem7  8065  cantnflem1c  8218  cantnflem1  8220  rankunb  8347  tcrank  8381  carduni  8441  dfac8alem  8486  acni  8502  alephinit  8552  aceq3lem  8577  dfac5  8585  dfac12lem2  8600  dfac12r  8602  dfac12k  8603  pwsdompw  8660  cflm  8706  fin1ai  8749  fin2i  8751  isfin2-2  8775  fin23lem17  8794  fin23lem39  8806  isf32lem1  8809  isf32lem2  8810  isf34lem4  8833  hsmexlem4  8885  axcc3  8894  domtriomlem  8898  axdc3lem2  8907  axdc4lem  8911  axcclem  8913  ttukeylem5  8969  ttukeylem6  8970  axdclem  8975  alephval2  9023  canth4  9098  pwfseqlem5  9114  winainflem  9144  wununi  9157  wunpw  9158  eltskm  9294  dedekind  9823  squeeze0  10537  fiminre  10583  lbreu  10584  nnsub  10676  ublbneg  11277  zsupss  11282  uzwo3  11288  zmax  11290  zbtwnre  11291  xrub  11626  infmremnf  11662  infmrp1  11663  fzrevral  11908  axdc4uzlem  12227  seqcl2  12263  seqcl  12265  seqf  12266  seqfveq2  12267  seqfveq  12269  seqshft2  12271  monoord  12275  monoord2  12276  sermono  12277  seqsplit  12278  seqcaopr3  12280  seqid  12290  seqid2  12291  seqhomo  12292  seqz  12293  discr1  12440  discr  12441  faclbnd4lem4  12513  hashbclem  12648  wrdind  12870  wrd2ind  12871  reuccats1lem  12873  recan  13448  cau3lem  13466  caubnd2  13469  limsupgre  13591  limsupgreOLD  13592  climi  13623  rlimi  13626  rlimclim1  13658  rlimclim  13659  climrlim2  13660  climshftlem  13687  rlimcld2  13691  rlimcn1  13701  climcn1  13704  subcn2  13707  isercoll  13780  isercoll2  13781  climcau  13783  caucvgrlem  13785  caucvgrlemOLD  13786  caucvgb  13795  serf0  13796  iseraltlem2  13798  iseraltlem3  13799  iseralt  13800  fsumm1  13861  fsum1p  13863  fsumcom2  13884  fsumge1  13906  telfsumo  13911  telfsumo2  13912  fsumparts  13915  o1fsum  13922  isum1p  13948  isumnn0nn  13949  isumrpcl  13950  climcndslem1  13956  climcndslem2  13957  climcnds  13958  cvgrat  13988  mertenslem1  13989  mertens  13991  clim2prod  13993  ntrivcvgfvn0  14004  fprodm1  14070  fprod1p  14071  fprodcom2  14087  sqrt2irr  14350  ndvdssub  14437  lcmf  14655  lcmfunsnlem1  14659  lcmfunsnlem2lem1  14660  lcmfunsnlem2lem2  14661  lcmfdvds  14664  lcmfdvdsb  14665  lcmfunsn  14666  prmind2  14684  nprm  14687  dvdsprm  14696  coprmgcdb  14703  coprm  14706  coprmprod  14727  coprmproddvdslem  14728  pcmpt  14886  pcmpt2  14887  pcmptdvds  14888  pcfac  14893  prmpwdvds  14897  unbenlem  14901  prmreclem4  14912  prmreclem5  14913  vdwlem1  14980  vdwlem2  14981  vdwlem9  14988  vdwlem10  14989  vdwlem13  14992  vdwnnlem1  14994  rami  15021  ramcl  15036  prmdvdsprmop  15050  prmodvdslcmf  15054  prmgaplcmlem1  15058  prmgaplcmlem1OLD  15061  prmdvdsprmorpOLD  15065  prmordvdslcmfOLD  15068  prmordvdslcmsOLDOLD  15070  prmgaplem7  15076  catidex  15629  catideu  15630  iscatd2  15636  catlid  15638  catrid  15639  subcidcl  15798  funcid  15824  initoid  15949  termoid  15950  initoeu1  15955  termoeu1  15962  yonedalem4c  16211  yonffthlem  16216  isdrs2  16233  lublecllem  16283  lubun  16418  poslubmo  16441  posglbmo  16442  sgrp2rid2ex  16710  grpidd2  16752  mulgsubcl  16821  issubg4  16885  ghmf1  16960  fislw  17326  efgi  17418  efgi2  17424  efgsdmi  17431  efgsrel  17433  gexexlem  17539  gsumzaddlem  17603  gsummhm2  17621  dprdcntz  17689  dprddisj  17690  dprdss  17711  dprd2dlem2  17722  dprd2da  17724  dpjrid  17744  ablfac1eu  17755  pgpfac1lem1  17756  pgpfaclem2  17764  srgrz  17808  srglz  17809  srgisid  17810  f1rhm0to0ALT  18018  issrngd  18138  islmodd  18146  islmhm2  18310  islbs2  18426  lbsextlem4  18433  rrgeq0i  18562  mvrf1  18698  mplsubglem  18707  mpllsslem  18708  subrgasclcl  18771  cply1mul  18936  prmirredlem  19113  ip2eq  19269  frlmphl  19388  mdetralt  19682  isclo2  20153  lmcvg  20327  cnpnei  20329  iscncl  20334  cncls  20339  lmss  20363  lmff  20366  cnt0  20411  isnrm2  20423  cnrmi  20425  isreg2  20442  cmpcov  20453  tgcmp  20465  uncmp  20467  fiuncmp  20468  dfcon2  20483  1stcclb  20508  1stcfb  20509  2ndcctbss  20519  1stcelcls  20525  restnlly  20546  islly2  20548  lly1stc  20560  comppfsc  20596  kgeni  20601  kgencn2  20621  ptpjpre1  20635  ptbasfi  20645  ptpjopn  20676  dfac14  20682  txtube  20704  txlm  20712  cnmpt11  20727  cnmpt21  20735  cnmptkp  20744  cnmptk1p  20749  qtopomap  20782  qtopcmap  20783  kqfvima  20794  kqt0lem  20800  isr0  20801  nrmr0reg  20813  fgss2  20938  isufil2  20972  cfinufil  20992  flimopn  21039  fbflim2  21041  flimcf  21046  flfneii  21056  cnpflf  21065  fclssscls  21082  fclsnei  21083  fclsrest  21088  fclscf  21089  flimfnfcls  21092  fclscmp  21094  isfcf  21098  fcfnei  21099  alexsubALTlem3  21113  alexsubALTlem4  21114  alexsubALT  21115  ptcmplem3  21118  tgpt0  21182  tsmsi  21197  tsmsgsum  21202  tsmsres  21207  tsmsxplem1  21216  tsmsxplem2  21217  tsmsxp  21218  ustincl  21271  ustdiag  21272  ustinvel  21273  ustexhalf  21274  ucnima  21345  ucncn  21349  cfiluexsm  21354  psmet0  21373  imasdsf1olem  21437  prdsbl  21555  metss  21572  comet  21577  metcnp3  21604  isngp4  21674  nmoi  21782  nmoiOLD  21798  mulc1cncf  21986  cncfco  21988  cnheiborlem  22031  cnheibor  22032  bndth  22035  lebnumii  22046  nmoleub2lem2  22179  nmoleub3  22182  ipcau2  22257  tchcphlem1  22258  tchcphlem2  22259  lmmcvg  22280  iscfil3  22292  iscau2  22296  iscau4  22298  cmetcaulem  22307  iscmet3lem1  22310  iscmet3lem2  22311  equivcfil  22318  equivcau  22319  lmcau  22331  pjthlem1  22440  pjthlem2  22441  ivthlem1  22451  ivthlem2  22452  ivthlem3  22453  ivth2  22455  ivthle  22456  ivthle2  22457  ivthicc  22458  ovoliunlem1  22504  ovolshftlem1  22511  ovolscalem1  22515  ovolicc2lem3  22521  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ovolicc2  22525  volsup  22558  dyadmbl  22607  vitalilem2  22616  vitalilem3  22617  mbfdm  22633  ismbf  22635  ismbf3d  22659  cncombf  22663  itg2seq  22749  itg2monolem2  22758  itg2monolem3  22759  itg2mono  22760  iblitg  22775  itgconst  22825  itgfsum  22833  limcvallem  22875  ellimc3  22883  cnlimci  22893  cnmptlimc  22894  dvferm1lem  22985  dvferm1  22986  dvferm2lem  22987  dvferm2  22988  dvlipcn  22995  dvle  23008  lhop1lem  23014  lhop1  23015  dvfsumge  23023  dvfsumlem2  23028  dvfsumlem3  23029  dvfsumlem4  23030  dvfsum2  23035  ftc1a  23038  ftc1lem4  23040  itgsubstlem  23049  fta1glem2  23166  fta1g  23167  plyeq0lem  23213  dgrcolem2  23277  dgrco  23278  plydivlem4  23298  plydivex  23299  fta1lem  23309  fta1  23310  vieta1lem2  23313  vieta1  23314  aalioulem2  23338  aalioulem4  23340  tayl0  23366  ulmi  23390  ulmclm  23391  ulmshftlem  23393  ulmcaulem  23398  ulmcau  23399  ulmcn  23403  ulmdvlem1  23404  ulmdvlem3  23406  ulmdv  23407  pserulm  23426  efif1olem4  23543  rlimcnp  23940  rlimcnp2  23941  xrlimcnp  23943  cxploglim  23952  scvxcvx  23960  lgamgulmlem5  24007  lgambdd  24011  lgamcvglem  24014  wilthlem2  24043  ftalem3  24048  fsumdvdscom  24163  musumsum  24170  chtub  24189  fsumvma  24190  perfectlem2  24207  dchrelbas3  24215  dchrelbasd  24216  dchrn0  24227  dchrptlem2  24242  lgsval2lem  24283  lgsdirnn0  24316  lgsdinn0  24317  2sqlem6  24346  2sqlem10  24351  dchrisumlema  24375  dchrisumlem1  24376  dchrisumlem2  24377  dchrisumlem3  24378  dchrmusum2  24381  dchrvmasumlem2  24385  dchrvmasumlem3  24386  dchrvmasumiflem1  24388  dchrisum0flblem2  24396  dchrisum0flb  24397  dchrisum0lem1b  24402  dchrisum0lem2  24405  2vmadivsumlem  24427  chpdifbndlem1  24440  selberg3lem1  24444  selberg4lem1  24447  pntrsumbnd2  24454  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem5  24468  pntrlog2bndlem6  24470  pntpbnd1  24473  pntibndlem2  24478  pntibndlem3  24479  pntibnd  24480  pntlemn  24487  pntlemj  24490  pntlemi  24491  pntlemo  24494  pntlem3  24496  pntleml  24498  ostth2lem1  24505  ostth2lem2  24521  ostth3  24525  brbtwn2  24984  colinearalg  24989  axcontlem4  25046  nbgra0nb  25206  nbgrassovt  25212  cusgrarn  25236  usgrasscusgra  25260  wwlknredwwlkn  25503  wwlkextproplem2  25519  clwwlkf1  25573  clwwlkext2edg  25579  clwwisshclwwlem1  25582  clwlkf1clwwlklem  25626  nbhashnn0  25691  rusgraprop4  25721  3cyclfrgrarn1  25789  n4cyclfrgra  25795  frgrawopreglem4  25824  frgrawopreg1  25827  frgrawopreg2  25828  extwwlkfablem2  25855  isgrpo  25973  isgrp2d  26012  opidonOLD  26099  exidu1  26103  rngoideu  26161  blocnilem  26494  ip2eqi  26547  ubthlem1  26561  minvecolem3  26567  minvecolem3OLD  26577  htthlem  26619  hial0  26804  hial02  26805  hial2eq  26808  ocorth  26993  occllem  27005  pjhthlem1  27093  h1de2i  27255  pjjsi  27402  lnopunilem1  27712  lnophmlem1  27718  nmcexi  27728  riesz4i  27765  mdi  27997  mdbr3  27999  mdbr4  28000  dmdi  28004  dmdbr3  28007  dmdbr4  28008  dmdi4  28009  mdslmd1i  28031  atss  28048  atom1d  28055  atmd  28101  sumdmdlem2  28121  cdj1i  28135  cdj3i  28143  nn0min  28433  archiabllem1a  28557  archiabllem2a  28560  archiabl  28564  isarchiofld  28629  crefi  28723  pcmplfin  28736  fmcncfil  28786  sigaclcu  28988  unelsiga  29005  sigapildsys  29033  ldgenpisys  29037  measvun  29080  mbfmcnvima  29128  carsgclctunlem2  29200  sibfima  29220  derangenlem  29943  subfacp1lem5  29956  subfacp1lem6  29957  rescon  30018  cvmcov  30035  cvmliftlem3  30059  cvmlift2lem10  30084  cvmliftphtlem  30089  mclsax  30256  ghomgrpilem1  30352  ghomf1olem  30361  dfon2lem6  30483  poseq  30540  soseq  30541  nocvxminlem  30628  nobndlem6  30635  fwddifnp1  30981  opnrebl2  31026  nn0prpwlem  31027  nn0prpw  31028  neibastop2lem  31065  neibastop2  31066  filnetlem4  31086  fin2so  31977  poimirlem25  32010  poimirlem29  32014  poimir  32018  mbfresfi  32032  ftc1cnnclem  32060  seqpo  32121  incsequz  32122  mettrifi  32131  geomcau  32133  caushft  32135  sstotbnd2  32151  equivtotbnd  32155  totbndbnd  32166  ismtybndlem  32183  heibor1lem  32186  bfplem2  32200  isdrngo2  32242  unichnidl  32309  lsat0cv  32644  lcvexchlem4  32648  lcvexchlem5  32649  eqlkr3  32712  lub0N  32800  glb0N  32804  cvrnbtwn  32882  ltrneq2  33758  trlval2  33774  lpolsatN  35101  lpolpolsatN  35102  hdmap14lem12  35495  incssnn0  35598  lnmlssfg  35983  unxpwdom3  35998  fnchoice  37390  limcrecl  37747  fourierdlem54  38062  fourierdlem103  38111  fourierdlem104  38112  smonoord  38756  iccpartlt  38776  iccpartgt  38779  iccpartdisj  38789  perfectALTVlem2  38882  bgoldbwt  38916  bgoldbst  38917  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  bgoldbnnsum3prm  38937  bgoldbtbndlem2  38939  bgoldbtbndlem3  38940  bgoldbtbndlem4  38941  bgoldbtbnd  38942  tgblthelfgott  38946  tgoldbach  38949  reuccatpfxs1lem  39014  usgruspgrb  39316  cusgredg  39542  cusgrres  39559  usgredgsscusgredg  39570  1wlk1walk  39697  1wlkdlem2  39726  upgrwlkdvdelem  39768  pthdlem2lem  39793  lfgrn1cycl  39824  lcosslsp  40504  linindslinci  40514  lindslinindsimp1  40523  ldepsnlinclem1  40571  ldepsnlinclem2  40572
  Copyright terms: Public domain W3C validator