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

Theorem csbeq1 3254
Description: Analog of dfsbcq 3163 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )

Proof of Theorem csbeq1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 3163 . . 3  |-  ( A  =  B  ->  ( [. A  /  x ]. y  e.  C  <->  [. B  /  x ]. y  e.  C )
)
21abbidv 2550 . 2  |-  ( A  =  B  ->  { y  |  [. A  /  x ]. y  e.  C }  =  { y  |  [. B  /  x ]. y  e.  C } )
3 df-csb 3252 . 2  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
4 df-csb 3252 . 2  |-  [_ B  /  x ]_ C  =  { y  |  [. B  /  x ]. y  e.  C }
52, 3, 43eqtr4g 2493 1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   {cab 2422   [.wsbc 3161   [_csb 3251
This theorem is referenced by:  csbeq1d  3257  csbeq1a  3259  csbiebg  3290  sbcnestgf  3298  cbvralcsf  3311  cbvreucsf  3313  cbvrabcsf  3314  csbing  3548  csbifg  3767  disjors  4198  disjxiun  4209  sbcbrg  4261  csbopabg  4283  pofun  4519  csbima12g  5213  csbiotag  5447  fvmpts  5807  fvmpt2i  5811  fvmptex  5815  fmptcof  5902  fmptcos  5903  fliftfuns  6036  csbovg  6112  csbriotag  6562  eqerlem  6937  qliftfuns  6991  boxcutc  7105  iunfi  7394  wdom2d  7548  summolem2a  12509  sumsn  12534  sumsns  12536  fsum2dlem  12554  fsumcom2  12558  fsumshftm  12564  fsum0diag2  12566  fsumrlim  12590  fsumo1  12591  fsumiun  12600  pcmptdvds  13263  psrass1lem  16442  fiuncmp  17467  elmptrab  17859  ovolfiniun  19397  finiunmbl  19438  volfiniun  19441  iundisj  19442  iundisj2  19443  iunmbl  19447  itgfsum  19718  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  dvfsumlem3  19912  dvfsumlem4  19913  dvfsum2  19918  itgsubstlem  19932  itgsubst  19933  rlimcnp2  20805  fsumdvdscom  20970  fsumdvdsmul  20980  fsumvma  20997  dchrisumlem2  21184  fargshiftfva  21626  ifeqeqx  24001  disji2f  24019  disjorsf  24022  disjif2  24023  disjabrex  24024  disjabrexf  24025  disjxpin  24028  iundisjf  24029  iundisj2f  24030  fvmpt2f  24072  funcnv4mpt  24085  iundisjfi  24152  iundisj2fi  24153  prodmolem2a  25260  prodsn  25286  fprodm1s  25293  fprodp1s  25294  prodsns  25295  fprod2dlem  25304  fprodcom2  25308  mzpsubst  26805  rabdiophlem2  26862  elnn0rabdioph  26863  dvdsrabdioph  26870  fphpd  26877  monotuz  27004  oddcomabszz  27007  fnwe2lem3  27127  flcidc  27356  sumsnd  27673  csbafv12g  27977  csbaovg  28020  cdlemk54  31755
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-sbc 3162  df-csb 3252
  Copyright terms: Public domain W3C validator