Theorem rspcv 3012

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 1626	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspc 3010	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721   A.wral 2670

This theorem is referenced by:  rspccv  3013  rspcva  3014  rspccva  3015  rspc3v  3025  rr19.3v  3041  rr19.28v  3042  rspsbc  3203  intmin  4034  somo  4501  fr2nr  4524  ralxfrALT  4705  fr3nr  4723  limuni3  4795  tfinds  4802  funcnvuni  5481  weniso  6038  knatar  6043  grprinvlem  6248  grprinvd  6249  caofref  6293  onnseq  6569  smo11  6589  tfrlem2  6600  tfrlem9  6609  tz7.49  6665  omeulem1  6788  oeordi  6793  nneneq  7253  frfi  7315  unblem2  7323  unbnn2  7327  xpfi  7341  ordiso2  7444  ordtypelem6  7452  ordtypelem7  7453  cantnflem1c  7603  cantnflem1  7605  rankunb  7736  tcrank  7768  carduni  7828  dfac8alem  7870  acni  7886  alephinit  7936  aceq3lem  7961  dfac5  7969  dfac12lem2  7984  dfac12r  7986  dfac12k  7987  pwsdompw  8044  cflm  8090  fin1ai  8133  fin2i  8135  isfin2-2  8159  fin23lem17  8178  fin23lem39  8190  isf32lem1  8193  isf32lem2  8194  isf34lem4  8217  hsmexlem4  8269  axcc3  8278  domtriomlem  8282  axdc3lem2  8291  axdc4lem  8295  axcclem  8297  ttukeylem5  8353  ttukeylem6  8354  axdclem  8359  alephval2  8407  canth4  8482  pwfseqlem5  8498  winainflem  8528  wununi  8541  wunpw  8542  eltskm  8678  squeeze0  9873  lbreu  9918  nnsub  9998  ublbneg  10520  zsupss  10525  uzwo3  10529  zmax  10531  zbtwnre  10532  xrub  10850  fzrevral  11090  axdc4uzlem  11280  seqcl2  11300  seqcl  11302  seqf  11303  seqfveq2  11304  seqfveq  11306  seqshft2  11308  monoord  11312  monoord2  11313  sermono  11314  seqsplit  11315  seqcaopr3  11317  seqid  11327  seqid2  11328  seqhomo  11329  seqz  11330  discr1  11474  discr  11475  faclbnd4lem4  11546  hashbclem  11660  wrdind  11750  recan  12099  cau3lem  12117  caubnd2  12120  limsupgre  12234  climi  12263  rlimi  12266  rlimclim1  12298  rlimclim  12299  climrlim2  12300  climshftlem  12327  rlimcld2  12331  rlimcn1  12341  climcn1  12344  subcn2  12347  isercoll  12420  isercoll2  12421  climcau  12423  caucvgrlem  12425  caucvgb  12432  serf0  12433  iseraltlem2  12435  iseraltlem3  12436  iseralt  12437  fsumm1  12496  fsum1p  12498  fsumcom2  12517  fsumge1  12535  fsumtscopo  12540  fsumtscopo2  12541  fsumparts  12544  o1fsum  12551  isum1p  12580  isumnn0nn  12581  isumrpcl  12582  climcndslem1  12588  climcndslem2  12589  climcnds  12590  cvgrat  12619  mertenslem1  12620  mertens  12622  sqr2irr  12807  ndvdssub  12886  prmind2  13049  nprm  13052  dvdsprm  13058  coprm  13059  pcmpt  13220  pcmpt2  13221  pcmptdvds  13222  pcfac  13227  prmpwdvds  13231  unbenlem  13235  prmreclem4  13246  prmreclem5  13247  vdwlem1  13308  vdwlem2  13309  vdwlem9  13316  vdwlem10  13317  vdwlem13  13320  vdwnnlem1  13322  rami  13342  ramcl  13356  catidex  13858  catideu  13859  iscatd2  13865  catlid  13867  catrid  13868  subcidcl  14000  funcid  14026  yonedalem4c  14333  yonffthlem  14338  isdrs2  14355  lubid  14398  lubun  14509  poslubmo  14532  spwmo  14617  grpidd2  14801  mulgsubcl  14863  issubg4  14920  ghmf1  14993  fislw  15218  efgi  15310  efgi2  15316  efgsdmi  15323  efgsrel  15325  gexexlem  15426  gsumzaddlem  15485  gsummhm2  15494  dprdcntz  15525  dprddisj  15526  dprdss  15546  dprd2dlem2  15557  dprd2da  15559  dpjrid  15579  ablfac1eu  15590  pgpfac1lem1  15591  pgpfaclem2  15599  issrngd  15908  islmodd  15915  islmhm2  16073  islbs2  16185  lbsextlem4  16192  rrgeq0i  16308  mvrf1  16448  mplsubglem  16457  mpllsslem  16458  subrgasclcl  16518  prmirredlem  16732  ip2eq  16843  isclo2  17111  lmcvg  17284  cnpnei  17286  iscncl  17291  cncls  17296  lmss  17320  lmff  17323  cnt0  17368  isnrm2  17380  cnrmi  17382  isreg2  17399  cmpcov  17410  tgcmp  17422  uncmp  17424  fiuncmp  17425  dfcon2  17439  1stcclb  17464  1stcfb  17465  2ndcctbss  17475  1stcelcls  17481  restnlly  17502  islly2  17504  lly1stc  17516  kgeni  17526  kgencn2  17546  ptpjpre1  17560  ptbasfi  17570  ptpjopn  17601  dfac14  17607  txtube  17629  txlm  17637  cnmpt11  17652  cnmpt21  17660  cnmptkp  17669  cnmptk1p  17674  qtopomap  17707  qtopcmap  17708  kqfvima  17719  kqt0lem  17725  isr0  17726  nrmr0reg  17738  fgss2  17863  isufil2  17897  cfinufil  17917  flimopn  17964  fbflim2  17966  flimcf  17971  flfneii  17981  cnpflf  17990  fclssscls  18007  fclsnei  18008  fclsrest  18013  fclscf  18014  flimfnfcls  18017  fclscmp  18019  isfcf  18023  fcfnei  18024  alexsubALTlem3  18037  alexsubALTlem4  18038  alexsubALT  18039  ptcmplem3  18042  tgpt0  18105  tsmsi  18120  tsmsgsum  18125  tsmsres  18130  tsmsxplem1  18139  tsmsxplem2  18140  tsmsxp  18141  ustincl  18194  ustdiag  18195  ustinvel  18196  ustexhalf  18197  isucn2  18266  ucnima  18268  ucncn  18272  cfiluexsm  18277  psmet0  18296  imasdsf1olem  18360  prdsbl  18478  metss  18495  comet  18500  metcnp3  18527  isngp4  18615  nmoi  18719  mulc1cncf  18892  cncfco  18894  cnheiborlem  18936  cnheibor  18937  bndth  18940  lebnumii  18948  nmoleub2lem2  19081  nmoleub3  19084  ipcau2  19148  tchcphlem1  19149  tchcphlem2  19150  lmmcvg  19171  iscfil3  19183  iscau2  19187  iscau4  19189  cmetcaulem  19198  iscmet3lem1  19201  iscmet3lem2  19202  equivcfil  19209  equivcau  19210  lmcau  19222  pjthlem1  19295  pjthlem2  19296  ivthlem1  19305  ivthlem2  19306  ivthlem3  19307  ivth2  19309  ivthle  19310  ivthle2  19311  ivthicc  19312  ovoliunlem1  19355  ovolshftlem1  19362  ovolscalem1  19366  ovolicc2lem3  19372  ovolicc2lem4  19373  ovolicc2  19375  volsup  19407  dyadmbl  19449  vitalilem2  19458  vitalilem3  19459  mbfdm  19477  ismbf  19479  ismbf3d  19503  cncombf  19507  itg2seq  19591  itg2monolem2  19600  itg2monolem3  19601  itg2mono  19602  iblitg  19617  itgconst  19667  itgfsum  19675  limcvallem  19715  ellimc3  19723  cnlimci  19733  cnmptlimc  19734  dvferm1lem  19825  dvferm1  19826  dvferm2lem  19827  dvferm2  19828  dvlipcn  19835  dvle  19848  lhop1lem  19854  lhop1  19855  dvfsumge  19863  dvfsumlem2  19868  dvfsumlem3  19869  dvfsumlem4  19870  dvfsum2  19875  ftc1a  19878  ftc1lem4  19880  itgsubstlem  19889  fta1glem2  20046  fta1g  20047  plyeq0lem  20086  dgrcolem2  20149  dgrco  20150  plydivlem4  20170  plydivex  20171  fta1lem  20181  fta1  20182  vieta1lem2  20185  vieta1  20186  aalioulem2  20207  aalioulem4  20209  tayl0  20235  ulmi  20259  ulmclm  20260  ulmshftlem  20262  ulmcaulem  20267  ulmcau  20268  ulmcn  20272  ulmdvlem1  20273  ulmdvlem3  20275  ulmdv  20276  pserulm  20295  efif1olem4  20404  rlimcnp  20761  rlimcnp2  20762  xrlimcnp  20764  cxploglim  20773  scvxcvx  20781  wilthlem2  20809  ftalem3  20814  fsumdvdscom  20927  musumsum  20934  chtub  20953  fsumvma  20954  perfectlem2  20971  dchrelbas3  20979  dchrelbasd  20980  dchrn0  20991  dchrptlem2  21006  lgsval2lem  21047  lgsdirnn0  21080  lgsdinn0  21081  2sqlem6  21110  2sqlem10  21115  dchrisumlema  21139  dchrisumlem1  21140  dchrisumlem2  21141  dchrisumlem3  21142  dchrmusum2  21145  dchrvmasumlem2  21149  dchrvmasumlem3  21150  dchrvmasumiflem1  21152  dchrisum0flblem2  21160  dchrisum0flb  21161  dchrisum0lem1b  21166  dchrisum0lem2  21169  2vmadivsumlem  21191  chpdifbndlem1  21204  selberg3lem1  21208  selberg4lem1  21211  pntrsumbnd2  21218  pntrlog2bndlem2  21229  pntrlog2bndlem3  21230  pntrlog2bndlem5  21232  pntrlog2bndlem6  21234  pntpbnd1  21237  pntibndlem2  21242  pntibndlem3  21243  pntibnd  21244  pntlemn  21251  pntlemj  21254  pntlemi  21255  pntlemo  21258  pntlem3  21260  pntleml  21262  ostth2lem1  21269  ostth2lem2  21285  ostth3  21289  nbgra0nb  21398  nbgrassovt  21404  cusgrarn  21425  usgrasscusgra  21449  isgrpo  21741  isgrp2d  21780  opidon  21867  exidu1  21871  rngoideu  21929  blocnilem  22262  ip2eqi  22315  ubthlem1  22329  minvecolem3  22335  htthlem  22377  hial0  22561  hial02  22562  hial2eq  22565  ocorth  22750  occllem  22762  pjhthlem1  22850  h1de2i  23012  pjjsi  23159  lnopunilem1  23470  lnophmlem1  23476  nmcexi  23486  riesz4i  23523  mdi  23755  mdbr3  23757  mdbr4  23758  dmdi  23762  dmdbr3  23765  dmdbr4  23766  dmdi4  23767  mdslmd1i  23789  atss  23806  atom1d  23813  atmd  23859  sumdmdlem2  23879  cdj1i  23893  cdj3i  23901  ofldadd  24195  ofldmul  24196  fmcncfil  24274  sigaclcu  24457  unelsiga  24474  measvun  24520  mbfmcnvima  24564  sibfima  24610  lgamgulmlem5  24774  lgambdd  24778  lgamcvglem  24781  derangenlem  24814  subfacp1lem5  24827  subfacp1lem6  24828  rescon  24890  cvmcov  24907  cvmliftlem3  24931  cvmlift2lem10  24956  cvmliftphtlem  24961  ghomgrpilem1  25053  ghomf1olem  25062  dedekind  25144  clim2prod  25173  ntrivcvgfvn0  25184  fprodm1  25247  fprod1p  25248  fprodcom2  25265  dfon2lem6  25362  poseq  25471  soseq  25472  nocvxminlem  25562  nobndlem6  25569  brbtwn2  25752  colinearalg  25757  axcontlem4  25814  mbfresfi  26156  ftc1cnnclem  26181  opnrebl2  26218  nn0prpwlem  26219  nn0prpw  26220  comppfsc  26281  neibastop2lem  26283  neibastop2  26284  filnetlem4  26304  seqpo  26345  incsequz  26346  mettrifi  26357  geomcau  26359  caushft  26361  sstotbnd2  26377  equivtotbnd  26381  totbndbnd  26392  ismtybndlem  26409  heibor1lem  26412  bfplem2  26426  isdrngo2  26468  unichnidl  26535  incssnn0  26659  lnmlssfg  27050  unxpwdom3  27128  fnchoice  27571  3cyclfrgrarn1  28120  n4cyclfrgra  28126  frgrawopreglem4  28154  frgrawopreg1  28157  frgrawopreg2  28158  lubunNEW  29460  lsat0cv  29520  lcvexchlem4  29524  lcvexchlem5  29525  eqlkr3  29588  lub0N  29676  glb0N  29680  cvrnbtwn  29758  ltrneq2  30634  trlval2  30649  lpolsatN  31975  lpolpolsatN  31976  hdmap14lem12  32369

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 2389

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 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ral 2675  df-v 2922