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

Theorem csbeq1a 3251
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 3250 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 3246 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2syl5eqr 2481 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   [_csb 3243
This theorem is referenced by:  csbhypf  3278  csbiebt  3279  sbcnestgf  3290  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306  csbing  3540  csbifg  3759  disjors  4190  disjxiun  4201  disjxun  4202  sbcbrg  4253  moop2  4443  pofun  4511  eusvnf  4709  reusv2lem4  4718  reusv2  4720  opeliunxp  4920  elrnmpt1  5110  csbima12g  5204  fvmpts  5798  fvmpt2i  5802  fvmptex  5806  fmptco  5892  fmptcof  5893  fmptcos  5894  elabrex  5976  fliftfuns  6027  csbovg  6103  ovmpt2s  6188  csbopeq1a  6391  mpt2mptsx  6405  dmmpt2ssx  6407  fmpt2x  6408  ovmptss  6419  fmpt2co  6421  riotasv2s  6587  eqerlem  6928  qliftfuns  6982  mptelixpg  7090  boxcutc  7096  xpf1o  7260  iunfi  7385  wdom2d  7537  ixpiunwdom  7548  hsmexlem2  8296  ac6num  8348  ac6c4  8350  iundom2g  8404  seqof2  11369  rlimcld2  12360  sumeq2w  12474  sumeq2ii  12475  summolem3  12496  summolem2a  12497  zsum  12500  fsum  12502  sumss2  12508  fsumcvg2  12509  sumsn  12522  sumsns  12524  fsum2dlem  12542  fsumcnv  12545  fsumcom2  12546  fsumshftm  12552  fsum0diag2  12554  fsum00  12565  fsumabs  12568  fsumrlim  12578  fsumo1  12579  o1fsum  12580  fsumiun  12588  infcvgaux1i  12624  pcmpt  13249  pcmptdvds  13251  natpropd  14161  fucpropd  14162  gsumcom2  15537  dprd2d2  15590  psrass1lem  16430  fiuncmp  17455  ptcld  17633  ptcldmpt  17634  ptclsg  17635  elmptrab  17847  prdsdsf  18385  prdsxmet  18387  fsumcn  18888  fsum2cn  18889  ovolfiniun  19385  ovoliunlem3  19388  ovoliun  19389  ovoliun2  19390  ovoliunnul  19391  finiunmbl  19426  volfiniun  19429  iundisj  19430  iundisj2  19431  iunmbl  19435  iunmbl2  19439  itgss3  19694  itgfsum  19706  itgabs  19714  limciun  19769  dvmptfsum  19847  dvfsumle  19893  dvfsumabs  19895  dvfsumlem1  19898  dvfsumlem2  19899  dvfsumlem3  19900  dvfsumlem4  19901  dvfsumrlim  19903  dvfsumrlim2  19904  dvfsum2  19906  itgsubstlem  19920  itgsubst  19921  mpfrcl  19927  rlimcnp2  20793  fsumdvdscom  20958  fsumdvdsmul  20968  fsumvma  20985  dchrisumlema  21170  dchrisumlem2  21172  dchrisumlem3  21173  ifeqeqx  23989  disjorsf  24010  disjabrex  24012  disjabrexf  24013  iundisjf  24017  iundisj2f  24018  suppss2f  24037  fmptdF  24057  resmptf  24059  fvmpt2f  24060  fmptcof2  24064  funcnv4mpt  24073  iundisjfi  24140  iundisj2fi  24141  esumpfinvalf  24454  measiun  24560  voliune  24573  volfiniune  24574  sbcung  25112  sbcopg  25114  prodeq2w  25227  prodeq2ii  25228  prodmolem3  25248  prodmolem2a  25249  zprod  25252  fprod  25256  fprodntriv  25257  prodss  25262  fprodser  25264  prodsn  25275  fprodm1s  25282  fprodp1s  25283  prodsns  25284  fprodabs  25286  fprodefsum  25287  fprodn0  25292  fprod2dlem  25293  fprodcnv  25296  fprodcom2  25297  sbcaltop  25774  itgabsnc  26220  ofmpteq  26713  mzpsubst  26742  rabdiophlem2  26799  elnn0rabdioph  26800  dvdsrabdioph  26807  fphpd  26814  monotuz  26941  oddcomabszz  26944  aomclem6  27071  flcidc  27294  fsumcnf  27606  sumsnd  27611  csbafv12g  27915  csbaovg  27958  cdleme31sn  31016  cdleme31sn1  31017  cdleme31se2  31019  cdleme32fva  31073  cdleme42b  31114  hlhilset  32574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-sbc 3154  df-csb 3244
  Copyright terms: Public domain W3C validator