Theorem rspcv 2880

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

Step	Hyp	Ref	Expression
1		nfv 1605	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspc 2878	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1623   e. wcel 1684   A.wral 2543

This theorem is referenced by:  rspccv  2881  rspcva  2882  rspccva  2883  rspc3v  2893  rr19.3v  2909  rr19.28v  2910  rspsbc  3069  intmin  3882  somo  4348  fr2nr  4371  ralxfrALT  4553  fr3nr  4571  limuni3  4643  tfinds  4650  funcnvuni  5317  weniso  5852  knatar  5857  grprinvlem  6058  grprinvd  6059  caofref  6103  onnseq  6361  smo11  6381  tfrlem2  6392  tfrlem9  6401  tz7.49  6457  omeulem1  6580  oeordi  6585  nneneq  7044  frfi  7102  unblem2  7110  unbnn2  7114  xpfi  7128  ordiso2  7230  ordtypelem6  7238  ordtypelem7  7239  cantnflem1c  7389  cantnflem1  7391  rankunb  7522  tcrank  7554  carduni  7614  dfac8alem  7656  acni  7672  alephinit  7722  aceq3lem  7747  dfac5  7755  dfac12lem2  7770  dfac12r  7772  dfac12k  7773  pwsdompw  7830  cflm  7876  fin1ai  7919  fin2i  7921  isfin2-2  7945  fin23lem17  7964  fin23lem39  7976  isf32lem1  7979  isf32lem2  7980  isf34lem4  8003  hsmexlem4  8055  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc4lem  8081  axcclem  8083  ttukeylem5  8140  ttukeylem6  8141  axdclem  8146  alephval2  8194  canth4  8269  pwfseqlem5  8285  winainflem  8315  wununi  8328  wunpw  8329  eltskm  8465  squeeze0  9659  lbreu  9704  nnsub  9784  ublbneg  10302  zsupss  10307  uzwo3  10311  zmax  10313  zbtwnre  10314  xrub  10630  fzrevral  10866  axdc4uzlem  11044  seqcl2  11064  seqcl  11066  seqf  11067  seqfveq2  11068  seqfveq  11070  seqshft2  11072  monoord  11076  monoord2  11077  sermono  11078  seqsplit  11079  seqcaopr3  11081  seqid  11091  seqid2  11092  seqhomo  11093  seqz  11094  discr1  11237  discr  11238  faclbnd4lem4  11309  hashbclem  11390  wrdind  11477  recan  11820  cau3lem  11838  caubnd2  11841  limsupgre  11955  climi  11984  rlimi  11987  rlimclim1  12019  rlimclim  12020  climrlim2  12021  climshftlem  12048  rlimcld2  12052  rlimcn1  12062  climcn1  12065  subcn2  12068  isercoll  12141  isercoll2  12142  climcau  12144  caucvgrlem  12145  caucvgb  12152  serf0  12153  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  fsumm1  12216  fsum1p  12218  fsumcom2  12237  fsumge1  12255  fsumtscopo  12260  fsumtscopo2  12261  fsumparts  12264  o1fsum  12271  isum1p  12300  isumnn0nn  12301  isumrpcl  12302  climcndslem1  12308  climcndslem2  12309  climcnds  12310  cvgrat  12339  mertenslem1  12340  mertens  12342  sqr2irr  12527  ndvdssub  12606  prmind2  12769  nprm  12772  dvdsprm  12778  coprm  12779  pcmpt  12940  pcmpt2  12941  pcmptdvds  12942  pcfac  12947  prmpwdvds  12951  unbenlem  12955  prmreclem4  12966  prmreclem5  12967  vdwlem1  13028  vdwlem2  13029  vdwlem9  13036  vdwlem10  13037  vdwlem13  13040  vdwnnlem1  13042  rami  13062  ramcl  13076  catidex  13576  catideu  13577  iscatd2  13583  catlid  13585  catrid  13586  subcidcl  13718  funcid  13744  yonedalem4c  14051  yonffthlem  14056  isdrs2  14073  lubid  14116  lubun  14227  poslubmo  14250  spwmo  14335  grpidd2  14519  mulgsubcl  14581  issubg4  14638  ghmf1  14711  fislw  14936  efgi  15028  efgi2  15034  efgsdmi  15041  efgsrel  15043  gexexlem  15144  gsumzaddlem  15203  gsummhm2  15212  dprdcntz  15243  dprddisj  15244  dprdss  15264  dprd2dlem2  15275  dprd2da  15277  dpjrid  15297  ablfac1eu  15308  pgpfac1lem1  15309  pgpfaclem2  15317  issrngd  15626  islmodd  15633  islmhm2  15795  islbs2  15907  lbsextlem4  15914  rrgeq0i  16030  mvrf1  16170  mplsubglem  16179  mpllsslem  16180  subrgasclcl  16240  prmirredlem  16446  ip2eq  16557  isclo2  16825  lmcvg  16992  cnpnei  16993  iscncl  16998  cncls  17003  lmss  17026  lmff  17029  cnt0  17074  isnrm2  17086  cnrmi  17088  isreg2  17105  cmpcov  17116  tgcmp  17128  uncmp  17130  fiuncmp  17131  dfcon2  17145  1stcclb  17170  1stcfb  17171  2ndcctbss  17181  1stcelcls  17187  restnlly  17208  islly2  17210  lly1stc  17222  kgeni  17232  kgencn2  17252  ptpjpre1  17266  ptbasfi  17276  ptpjopn  17306  dfac14  17312  txtube  17334  txlm  17342  cnmpt11  17357  cnmpt21  17365  cnmptkp  17374  cnmptk1p  17379  qtopomap  17409  qtopcmap  17410  kqfvima  17421  kqt0lem  17427  isr0  17428  nrmr0reg  17440  fgss2  17569  isufil2  17603  cfinufil  17623  flimopn  17670  fbflim2  17672  flimcf  17677  flfneii  17687  cnpflf  17696  fclssscls  17713  fclsnei  17714  fclsrest  17719  fclscf  17720  flimfnfcls  17723  fclscmp  17725  isfcf  17729  fcfnei  17730  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem3  17748  tgpt0  17801  tsmsi  17816  tsmsgsum  17821  tsmsres  17826  tsmsxplem1  17835  tsmsxplem2  17836  tsmsxp  17837  imasdsf1olem  17937  prdsbl  18037  metss  18054  comet  18059  metcnp3  18086  isngp4  18133  nmoi  18237  mulc1cncf  18409  cncfco  18411  cnheiborlem  18452  cnheibor  18453  bndth  18456  lebnumii  18464  nmoleub2lem2  18597  nmoleub3  18600  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  lmmcvg  18687  iscfil3  18699  iscau2  18703  iscau4  18705  cmetcaulem  18714  iscmet3lem1  18717  iscmet3lem2  18718  equivcfil  18725  equivcau  18726  lmcau  18738  pjthlem1  18801  pjthlem2  18802  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ivthle  18816  ivthle2  18817  ivthicc  18818  ovoliunlem1  18861  ovolshftlem1  18868  ovolscalem1  18872  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2  18881  volsup  18913  dyadmbl  18955  vitalilem2  18964  vitalilem3  18965  mbfdm  18983  ismbf  18985  ismbf3d  19009  cncombf  19013  itg2seq  19097  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  iblitg  19123  itgconst  19173  itgfsum  19181  limcvallem  19221  ellimc3  19229  cnlimci  19239  cnmptlimc  19240  dvferm1lem  19331  dvferm1  19332  dvferm2lem  19333  dvferm2  19334  dvlipcn  19341  dvle  19354  lhop1lem  19360  lhop1  19361  dvfsumge  19369  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  itgsubstlem  19395  fta1glem2  19552  fta1g  19553  plyeq0lem  19592  dgrcolem2  19655  dgrco  19656  plydivlem4  19676  plydivex  19677  fta1lem  19687  fta1  19688  vieta1lem2  19691  vieta1  19692  aalioulem2  19713  aalioulem4  19715  tayl0  19741  ulmi  19765  ulmclm  19766  ulmshftlem  19768  ulmcaulem  19771  ulmcau  19772  ulmcn  19776  ulmdvlem1  19777  ulmdvlem3  19779  ulmdv  19780  pserulm  19798  efif1olem4  19907  rlimcnp  20260  rlimcnp2  20261  xrlimcnp  20263  cxploglim  20272  scvxcvx  20280  wilthlem2  20307  ftalem3  20312  fsumdvdscom  20425  musumsum  20432  chtub  20451  fsumvma  20452  perfectlem2  20469  dchrelbas3  20477  dchrelbasd  20478  dchrn0  20489  dchrptlem2  20504  lgsval2lem  20545  lgsdirnn0  20578  lgsdinn0  20579  2sqlem6  20608  2sqlem10  20613  dchrisumlema  20637  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0flb  20659  dchrisum0lem1b  20664  dchrisum0lem2  20667  2vmadivsumlem  20689  chpdifbndlem1  20702  selberg3lem1  20706  selberg4lem1  20709  pntrsumbnd2  20716  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntpbnd1  20735  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemn  20749  pntlemj  20752  pntlemi  20753  pntlemo  20756  pntlem3  20758  pntleml  20760  ostth2lem1  20767  ostth2lem2  20783  ostth3  20787  isgrpo  20863  isgrp2d  20902  opidon  20989  exidu1  20993  rngoideu  21051  blocnilem  21382  ip2eqi  21435  ubthlem1  21449  minvecolem3  21455  htthlem  21497  hial0  21681  hial02  21682  hial2eq  21685  ocorth  21870  occllem  21882  pjhthlem1  21970  h1de2i  22132  pjjsi  22279  lnopunilem1  22590  lnophmlem1  22596  nmcexi  22606  riesz4i  22643  mdi  22875  mdbr3  22877  mdbr4  22878  dmdi  22882  dmdbr3  22885  dmdbr4  22886  dmdi4  22887  mdslmd1i  22909  atss  22926  atom1d  22933  atmd  22979  sumdmdlem2  22999  cdj1i  23013  cdj3i  23021  sigaclcu  23478  unelsiga  23495  measvun  23537  mbfmcnvima  23562  derangenlem  23702  subfacp1lem5  23715  subfacp1lem6  23716  rescon  23777  cvmcov  23794  cvmliftlem3  23818  cvmlift2lem10  23843  cvmliftphtlem  23848  ghomgrpilem1  23992  ghomf1olem  24001  dedekind  24082  dfon2lem6  24144  poseq  24253  soseq  24254  nocvxminlem  24344  nobndlem6  24351  brbtwn2  24533  colinearalg  24538  axcontlem4  24595  dstr  25171  supdefa  25263  ridlideq  25335  basexre  25522  osneisi  25531  exopcopn  25572  limptlimpr2lem2  25575  bwt2  25592  supnuf  25629  pgapspf  26052  pgapspf2  26053  elhaltdp2  26068  tethpnc2  26071  isibg2aa  26112  isibg2aalem2  26114  isibg2aalem3  26115  opnrebl2  26236  nn0prpwlem  26238  nn0prpw  26239  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  filnetlem4  26330  seqpo  26457  incsequz  26458  mettrifi  26473  geomcau  26475  caushft  26477  sstotbnd2  26498  equivtotbnd  26502  totbndbnd  26513  ismtybndlem  26530  heibor1lem  26533  bfplem2  26547  isdrngo2  26589  unichnidl  26656  incssnn0  26786  lnmlssfg  27178  unxpwdom3  27256  fnchoice  27700  nbgra0nb  28144  nbgrassovt  28150  lubunNEW  29163  lsat0cv  29223  lcvexchlem4  29227  lcvexchlem5  29228  eqlkr3  29291  lub0N  29379  glb0N  29383  cvrnbtwn  29461  ltrneq2  30337  trlval2  30352  lpolsatN  31678  lpolpolsatN  31679  hdmap14lem12  32072

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790