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

Theorem csbeq1 3097
Description: Analog of dfsbcq 3006 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 3006 . . 3  |-  ( A  =  B  ->  ( [. A  /  x ]. y  e.  C  <->  [. B  /  x ]. y  e.  C )
)
21abbidv 2410 . 2  |-  ( A  =  B  ->  { y  |  [. A  /  x ]. y  e.  C }  =  { y  |  [. B  /  x ]. y  e.  C } )
3 df-csb 3095 . 2  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
4 df-csb 3095 . 2  |-  [_ B  /  x ]_ C  =  { y  |  [. B  /  x ]. y  e.  C }
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   {cab 2282   [.wsbc 3004   [_csb 3094
This theorem is referenced by:  csbeq1d  3100  csbeq1a  3102  csbiebg  3133  sbcnestgf  3141  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  csbing  3389  csbifg  3606  disjors  4025  disjxiun  4036  sbcbrg  4088  csbopabg  4110  pofun  4346  csbima12g  5038  csbiotag  5264  fvmpts  5619  fvmpt2i  5623  fvmptex  5626  fmptcof  5708  fmptcos  5709  fliftfuns  5829  csbovg  5905  csbriotag  6333  eqerlem  6708  qliftfuns  6761  boxcutc  6875  iunfi  7160  wdom2d  7310  summolem2a  12204  sumsn  12229  sumsns  12231  fsum2dlem  12249  fsumcom2  12253  fsumshftm  12259  fsum0diag2  12261  fsumrlim  12285  fsumo1  12286  fsumiun  12295  pcmptdvds  12958  psrass1lem  16139  fiuncmp  17147  elmptrab  17538  ovolfiniun  18876  finiunmbl  18917  volfiniun  18920  iundisj  18921  iundisj2  18922  iunmbl  18926  itgfsum  19197  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsum2  19397  itgsubstlem  19411  itgsubst  19412  rlimcnp2  20277  fsumdvdscom  20441  fsumdvdsmul  20451  fsumvma  20468  dchrisumlem2  20655  ifeqeqx  23050  fvmpt2f  23239  funcnv4mpt  23252  disji2f  23369  disjorsf  23372  disjif2  23373  disjabrex  23374  disjabrexf  23375  iundisjfi  23378  iundisj2fi  23379  iundisjf  23380  iundisj2f  23381  prodmolem2a  24157  fprod1s  25428  fprodp1s  25430  mzpsubst  26929  rabdiophlem2  26986  elnn0rabdioph  26987  dvdsrabdioph  26994  fphpd  27002  monotuz  27129  oddcomabszz  27132  fnwe2lem3  27252  flcidc  27482  sumsnd  27800  csbafv12g  28105  csbaovg  28148  fargshiftfva  28384  cdlemk54  31769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator