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

Theorem csbeq1a 3275
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 3274 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 3270 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2syl5eqr 2488 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   [_csb 3267
This theorem is referenced by:  csbhypf  3285  csbiebt  3286  cbvralcsf  3297  cbvreucsf  3299  cbvrabcsf  3300  sbcnestgf  3666  csbin  3685  csbingOLD  3686  csbifg  3791  disjors  4223  disjxiun  4234  disjxun  4235  sbcbrg  4286  moop2  4480  pofun  4548  eusvnf  4747  reusv2lem4  4756  reusv2  4758  opeliunxp  4958  elrnmpt1  5148  csbima12g  5242  fvmpts  5836  fvmpt2i  5840  fvmptex  5844  fmptco  5930  fmptcof  5931  fmptcos  5932  elabrex  6014  fliftfuns  6065  csbovg  6141  ovmpt2s  6226  csbopeq1a  6429  mpt2mptsx  6443  dmmpt2ssx  6445  fmpt2x  6446  ovmptss  6457  fmpt2co  6459  riotasv2s  6625  eqerlem  6966  qliftfuns  7020  mptelixpg  7128  boxcutc  7134  xpf1o  7298  iunfi  7423  wdom2d  7577  ixpiunwdom  7588  hsmexlem2  8338  ac6num  8390  ac6c4  8392  iundom2g  8446  seqof2  11412  rlimcld2  12403  sumeq2w  12517  sumeq2ii  12518  summolem3  12539  summolem2a  12540  zsum  12543  fsum  12545  sumss2  12551  fsumcvg2  12552  sumsn  12565  sumsns  12567  fsum2dlem  12585  fsumcnv  12588  fsumcom2  12589  fsumshftm  12595  fsum0diag2  12597  fsum00  12608  fsumabs  12611  fsumrlim  12621  fsumo1  12622  o1fsum  12623  fsumiun  12631  infcvgaux1i  12667  pcmpt  13292  pcmptdvds  13294  natpropd  14204  fucpropd  14205  gsumcom2  15580  dprd2d2  15633  psrass1lem  16473  fiuncmp  17498  ptcld  17676  ptcldmpt  17677  ptclsg  17678  elmptrab  17890  prdsdsf  18428  prdsxmet  18430  fsumcn  18931  fsum2cn  18932  ovolfiniun  19428  ovoliunlem3  19431  ovoliun  19432  ovoliun2  19433  ovoliunnul  19434  finiunmbl  19469  volfiniun  19472  iundisj  19473  iundisj2  19474  iunmbl  19478  iunmbl2  19482  itgss3  19735  itgfsum  19747  itgabs  19755  limciun  19812  dvmptfsum  19890  dvfsumle  19936  dvfsumabs  19938  dvfsumlem1  19941  dvfsumlem2  19942  dvfsumlem3  19943  dvfsumlem4  19944  dvfsumrlim  19946  dvfsumrlim2  19947  dvfsum2  19949  itgsubstlem  19963  itgsubst  19964  mpfrcl  19970  rlimcnp2  20836  fsumdvdscom  21001  fsumdvdsmul  21011  fsumvma  21028  dchrisumlema  21213  dchrisumlem2  21215  dchrisumlem3  21216  ifeqeqx  24032  disjorsf  24053  disjabrex  24055  disjabrexf  24056  iundisjf  24060  iundisj2f  24061  suppss2f  24080  fmptdF  24100  resmptf  24102  fvmpt2f  24103  fmptcof2  24107  funcnv4mpt  24116  iundisjfi  24183  iundisj2fi  24184  esumpfinvalf  24497  measiun  24603  voliune  24616  volfiniune  24617  sbcung  25155  sbcopg  25157  prodeq2w  25269  prodeq2ii  25270  prodmolem3  25290  prodmolem2a  25291  zprod  25294  fprod  25298  fprodntriv  25299  prodss  25304  fprodser  25306  prodsn  25317  fprodm1s  25324  fprodp1s  25325  prodsns  25326  fprodabs  25328  fprodefsum  25329  fprodn0  25334  fprod2dlem  25335  fprodcnv  25338  fprodcom2  25339  sbcaltop  25857  itgabsnc  26312  ftc1cnnclem  26316  ftc2nc  26327  ofmpteq  26814  mzpsubst  26843  rabdiophlem2  26900  elnn0rabdioph  26901  dvdsrabdioph  26908  fphpd  26915  monotuz  27042  oddcomabszz  27045  aomclem6  27172  flcidc  27394  fsumcnf  27706  sumsnd  27711  csbafv12g  28015  csbaovg  28058  cdleme31sn  31275  cdleme31sn1  31276  cdleme31se2  31278  cdleme32fva  31332  cdleme42b  31373  hlhilset  32833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-sbc 3168  df-csb 3268
  Copyright terms: Public domain W3C validator