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

Theorem rspcv 3050
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 1630 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3048 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   A.wral 2707
This theorem is referenced by:  rspccv  3051  rspcva  3052  rspccva  3053  rspc3v  3063  rr19.3v  3079  rr19.28v  3080  rspsbc  3241  intmin  4072  somo  4539  fr2nr  4562  ralxfrALT  4744  fr3nr  4762  limuni3  4834  tfinds  4841  funcnvuni  5520  weniso  6077  knatar  6082  grprinvlem  6287  grprinvd  6288  caofref  6332  onnseq  6608  smo11  6628  tfrlem2  6639  tfrlem9  6648  tz7.49  6704  omeulem1  6827  oeordi  6832  nneneq  7292  frfi  7354  unblem2  7362  unbnn2  7366  xpfi  7380  ordiso2  7486  ordtypelem6  7494  ordtypelem7  7495  cantnflem1c  7645  cantnflem1  7647  rankunb  7778  tcrank  7810  carduni  7870  dfac8alem  7912  acni  7928  alephinit  7978  aceq3lem  8003  dfac5  8011  dfac12lem2  8026  dfac12r  8028  dfac12k  8029  pwsdompw  8086  cflm  8132  fin1ai  8175  fin2i  8177  isfin2-2  8201  fin23lem17  8220  fin23lem39  8232  isf32lem1  8235  isf32lem2  8236  isf34lem4  8259  hsmexlem4  8311  axcc3  8320  domtriomlem  8324  axdc3lem2  8333  axdc4lem  8337  axcclem  8339  ttukeylem5  8395  ttukeylem6  8396  axdclem  8401  alephval2  8449  canth4  8524  pwfseqlem5  8540  winainflem  8570  wununi  8583  wunpw  8584  eltskm  8720  squeeze0  9915  lbreu  9960  nnsub  10040  ublbneg  10562  zsupss  10567  uzwo3  10571  zmax  10573  zbtwnre  10574  xrub  10892  fzrevral  11133  axdc4uzlem  11323  seqcl2  11343  seqcl  11345  seqf  11346  seqfveq2  11347  seqfveq  11349  seqshft2  11351  monoord  11355  monoord2  11356  sermono  11357  seqsplit  11358  seqcaopr3  11360  seqid  11370  seqid2  11371  seqhomo  11372  seqz  11373  discr1  11517  discr  11518  faclbnd4lem4  11589  hashbclem  11703  wrdind  11793  recan  12142  cau3lem  12160  caubnd2  12163  limsupgre  12277  climi  12306  rlimi  12309  rlimclim1  12341  rlimclim  12342  climrlim2  12343  climshftlem  12370  rlimcld2  12374  rlimcn1  12384  climcn1  12387  subcn2  12390  isercoll  12463  isercoll2  12464  climcau  12466  caucvgrlem  12468  caucvgb  12475  serf0  12476  iseraltlem2  12478  iseraltlem3  12479  iseralt  12480  fsumm1  12539  fsum1p  12541  fsumcom2  12560  fsumge1  12578  fsumtscopo  12583  fsumtscopo2  12584  fsumparts  12587  o1fsum  12594  isum1p  12623  isumnn0nn  12624  isumrpcl  12625  climcndslem1  12631  climcndslem2  12632  climcnds  12633  cvgrat  12662  mertenslem1  12663  mertens  12665  sqr2irr  12850  ndvdssub  12929  prmind2  13092  nprm  13095  dvdsprm  13101  coprm  13102  pcmpt  13263  pcmpt2  13264  pcmptdvds  13265  pcfac  13270  prmpwdvds  13274  unbenlem  13278  prmreclem4  13289  prmreclem5  13290  vdwlem1  13351  vdwlem2  13352  vdwlem9  13359  vdwlem10  13360  vdwlem13  13363  vdwnnlem1  13365  rami  13385  ramcl  13399  catidex  13901  catideu  13902  iscatd2  13908  catlid  13910  catrid  13911  subcidcl  14043  funcid  14069  yonedalem4c  14376  yonffthlem  14381  isdrs2  14398  lubid  14441  lubun  14552  poslubmo  14575  spwmo  14660  grpidd2  14844  mulgsubcl  14906  issubg4  14963  ghmf1  15036  fislw  15261  efgi  15353  efgi2  15359  efgsdmi  15366  efgsrel  15368  gexexlem  15469  gsumzaddlem  15528  gsummhm2  15537  dprdcntz  15568  dprddisj  15569  dprdss  15589  dprd2dlem2  15600  dprd2da  15602  dpjrid  15622  ablfac1eu  15633  pgpfac1lem1  15634  pgpfaclem2  15642  issrngd  15951  islmodd  15958  islmhm2  16116  islbs2  16228  lbsextlem4  16235  rrgeq0i  16351  mvrf1  16491  mplsubglem  16500  mpllsslem  16501  subrgasclcl  16561  prmirredlem  16775  ip2eq  16886  isclo2  17154  lmcvg  17328  cnpnei  17330  iscncl  17335  cncls  17340  lmss  17364  lmff  17367  cnt0  17412  isnrm2  17424  cnrmi  17426  isreg2  17443  cmpcov  17454  tgcmp  17466  uncmp  17468  fiuncmp  17469  bwth  17475  dfcon2  17484  1stcclb  17509  1stcfb  17510  2ndcctbss  17520  1stcelcls  17526  restnlly  17547  islly2  17549  lly1stc  17561  kgeni  17571  kgencn2  17591  ptpjpre1  17605  ptbasfi  17615  ptpjopn  17646  dfac14  17652  txtube  17674  txlm  17682  cnmpt11  17697  cnmpt21  17705  cnmptkp  17714  cnmptk1p  17719  qtopomap  17752  qtopcmap  17753  kqfvima  17764  kqt0lem  17770  isr0  17771  nrmr0reg  17783  fgss2  17908  isufil2  17942  cfinufil  17962  flimopn  18009  fbflim2  18011  flimcf  18016  flfneii  18026  cnpflf  18035  fclssscls  18052  fclsnei  18053  fclsrest  18058  fclscf  18059  flimfnfcls  18062  fclscmp  18064  isfcf  18068  fcfnei  18069  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  ptcmplem3  18087  tgpt0  18150  tsmsi  18165  tsmsgsum  18170  tsmsres  18175  tsmsxplem1  18184  tsmsxplem2  18185  tsmsxp  18186  ustincl  18239  ustdiag  18240  ustinvel  18241  ustexhalf  18242  isucn2  18311  ucnima  18313  ucncn  18317  cfiluexsm  18322  psmet0  18341  imasdsf1olem  18405  prdsbl  18523  metss  18540  comet  18545  metcnp3  18572  isngp4  18660  nmoi  18764  mulc1cncf  18937  cncfco  18939  cnheiborlem  18981  cnheibor  18982  bndth  18985  lebnumii  18993  nmoleub2lem2  19126  nmoleub3  19129  ipcau2  19193  tchcphlem1  19194  tchcphlem2  19195  lmmcvg  19216  iscfil3  19228  iscau2  19232  iscau4  19234  cmetcaulem  19243  iscmet3lem1  19246  iscmet3lem2  19247  equivcfil  19254  equivcau  19255  lmcau  19267  pjthlem1  19340  pjthlem2  19341  ivthlem1  19350  ivthlem2  19351  ivthlem3  19352  ivth2  19354  ivthle  19355  ivthle2  19356  ivthicc  19357  ovoliunlem1  19400  ovolshftlem1  19407  ovolscalem1  19411  ovolicc2lem3  19417  ovolicc2lem4  19418  ovolicc2  19420  volsup  19452  dyadmbl  19494  vitalilem2  19503  vitalilem3  19504  mbfdm  19522  ismbf  19524  ismbf3d  19548  cncombf  19552  itg2seq  19636  itg2monolem2  19645  itg2monolem3  19646  itg2mono  19647  iblitg  19662  itgconst  19712  itgfsum  19720  limcvallem  19760  ellimc3  19768  cnlimci  19778  cnmptlimc  19779  dvferm1lem  19870  dvferm1  19871  dvferm2lem  19872  dvferm2  19873  dvlipcn  19880  dvle  19893  lhop1lem  19899  lhop1  19900  dvfsumge  19908  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumlem4  19915  dvfsum2  19920  ftc1a  19923  ftc1lem4  19925  itgsubstlem  19934  fta1glem2  20091  fta1g  20092  plyeq0lem  20131  dgrcolem2  20194  dgrco  20195  plydivlem4  20215  plydivex  20216  fta1lem  20226  fta1  20227  vieta1lem2  20230  vieta1  20231  aalioulem2  20252  aalioulem4  20254  tayl0  20280  ulmi  20304  ulmclm  20305  ulmshftlem  20307  ulmcaulem  20312  ulmcau  20313  ulmcn  20317  ulmdvlem1  20318  ulmdvlem3  20320  ulmdv  20321  pserulm  20340  efif1olem4  20449  rlimcnp  20806  rlimcnp2  20807  xrlimcnp  20809  cxploglim  20818  scvxcvx  20826  wilthlem2  20854  ftalem3  20859  fsumdvdscom  20972  musumsum  20979  chtub  20998  fsumvma  20999  perfectlem2  21016  dchrelbas3  21024  dchrelbasd  21025  dchrn0  21036  dchrptlem2  21051  lgsval2lem  21092  lgsdirnn0  21125  lgsdinn0  21126  2sqlem6  21155  2sqlem10  21160  dchrisumlema  21184  dchrisumlem1  21185  dchrisumlem2  21186  dchrisumlem3  21187  dchrmusum2  21190  dchrvmasumlem2  21194  dchrvmasumlem3  21195  dchrvmasumiflem1  21197  dchrisum0flblem2  21205  dchrisum0flb  21206  dchrisum0lem1b  21211  dchrisum0lem2  21214  2vmadivsumlem  21236  chpdifbndlem1  21249  selberg3lem1  21253  selberg4lem1  21256  pntrsumbnd2  21263  pntrlog2bndlem2  21274  pntrlog2bndlem3  21275  pntrlog2bndlem5  21277  pntrlog2bndlem6  21279  pntpbnd1  21282  pntibndlem2  21287  pntibndlem3  21288  pntibnd  21289  pntlemn  21296  pntlemj  21299  pntlemi  21300  pntlemo  21303  pntlem3  21305  pntleml  21307  ostth2lem1  21314  ostth2lem2  21330  ostth3  21334  nbgra0nb  21443  nbgrassovt  21449  cusgrarn  21470  usgrasscusgra  21494  isgrpo  21786  isgrp2d  21825  opidon  21912  exidu1  21916  rngoideu  21974  blocnilem  22307  ip2eqi  22360  ubthlem1  22374  minvecolem3  22380  htthlem  22422  hial0  22606  hial02  22607  hial2eq  22610  ocorth  22795  occllem  22807  pjhthlem1  22895  h1de2i  23057  pjjsi  23204  lnopunilem1  23515  lnophmlem1  23521  nmcexi  23531  riesz4i  23568  mdi  23800  mdbr3  23802  mdbr4  23803  dmdi  23807  dmdbr3  23810  dmdbr4  23811  dmdi4  23812  mdslmd1i  23834  atss  23851  atom1d  23858  atmd  23904  sumdmdlem2  23924  cdj1i  23938  cdj3i  23946  ofldadd  24240  ofldmul  24241  fmcncfil  24319  sigaclcu  24502  unelsiga  24519  measvun  24565  mbfmcnvima  24609  sibfima  24655  lgamgulmlem5  24819  lgambdd  24823  lgamcvglem  24826  derangenlem  24859  subfacp1lem5  24872  subfacp1lem6  24873  rescon  24935  cvmcov  24952  cvmliftlem3  24976  cvmlift2lem10  25001  cvmliftphtlem  25006  ghomgrpilem1  25098  ghomf1olem  25107  dedekind  25189  clim2prod  25218  ntrivcvgfvn0  25229  fprodm1  25292  fprod1p  25293  fprodcom2  25310  dfon2lem6  25417  poseq  25530  soseq  25531  nocvxminlem  25647  nobndlem6  25654  brbtwn2  25846  colinearalg  25851  axcontlem4  25908  mbfresfi  26255  ftc1cnnclem  26280  opnrebl2  26326  nn0prpwlem  26327  nn0prpw  26328  comppfsc  26389  neibastop2lem  26391  neibastop2  26392  filnetlem4  26412  seqpo  26453  incsequz  26454  mettrifi  26465  geomcau  26467  caushft  26469  sstotbnd2  26485  equivtotbnd  26489  totbndbnd  26500  ismtybndlem  26517  heibor1lem  26520  bfplem2  26534  isdrngo2  26576  unichnidl  26643  incssnn0  26767  lnmlssfg  27157  unxpwdom3  27235  fnchoice  27678  3cyclfrgrarn1  28464  n4cyclfrgra  28470  frgrawopreglem4  28498  frgrawopreg1  28501  frgrawopreg2  28502  lubunNEW  29833  lsat0cv  29893  lcvexchlem4  29897  lcvexchlem5  29898  eqlkr3  29961  lub0N  30049  glb0N  30053  cvrnbtwn  30131  ltrneq2  31007  trlval2  31022  lpolsatN  32348  lpolpolsatN  32349  hdmap14lem12  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960
  Copyright terms: Public domain W3C validator