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

Theorem csbeq1 3160
Description: Analog of dfsbcq 3069 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 3069 . . 3  |-  ( A  =  B  ->  ( [. A  /  x ]. y  e.  C  <->  [. B  /  x ]. y  e.  C )
)
21abbidv 2472 . 2  |-  ( A  =  B  ->  { y  |  [. A  /  x ]. y  e.  C }  =  { y  |  [. B  /  x ]. y  e.  C } )
3 df-csb 3158 . 2  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
4 df-csb 3158 . 2  |-  [_ B  /  x ]_ C  =  { y  |  [. B  /  x ]. y  e.  C }
52, 3, 43eqtr4g 2415 1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710   {cab 2344   [.wsbc 3067   [_csb 3157
This theorem is referenced by:  csbeq1d  3163  csbeq1a  3165  csbiebg  3196  sbcnestgf  3204  cbvralcsf  3219  cbvreucsf  3221  cbvrabcsf  3222  csbing  3452  csbifg  3669  disjors  4090  disjxiun  4101  sbcbrg  4153  csbopabg  4175  pofun  4412  csbima12g  5104  csbiotag  5330  fvmpts  5686  fvmpt2i  5690  fvmptex  5693  fmptcof  5775  fmptcos  5776  fliftfuns  5900  csbovg  5976  csbriotag  6404  eqerlem  6779  qliftfuns  6833  boxcutc  6947  iunfi  7234  wdom2d  7384  summolem2a  12285  sumsn  12310  sumsns  12312  fsum2dlem  12330  fsumcom2  12334  fsumshftm  12340  fsum0diag2  12342  fsumrlim  12366  fsumo1  12367  fsumiun  12376  pcmptdvds  13039  psrass1lem  16222  fiuncmp  17237  elmptrab  17624  ovolfiniun  18964  finiunmbl  19005  volfiniun  19008  iundisj  19009  iundisj2  19010  iunmbl  19014  itgfsum  19285  dvfsumle  19472  dvfsumabs  19474  dvfsumlem2  19478  dvfsumlem3  19479  dvfsumlem4  19480  dvfsum2  19485  itgsubstlem  19499  itgsubst  19500  rlimcnp2  20372  fsumdvdscom  20537  fsumdvdsmul  20547  fsumvma  20564  dchrisumlem2  20751  ifeqeqx  23200  disji2f  23218  disjorsf  23221  disjif2  23222  disjabrex  23223  disjabrexf  23224  iundisjf  23227  iundisj2f  23228  fvmpt2f  23275  funcnv4mpt  23288  iundisjfi  23356  iundisj2fi  23357  prodmolem2a  24561  prodsn  24587  fprodm1s  24594  fprodp1s  24595  prodsns  24596  mzpsubst  26149  rabdiophlem2  26206  elnn0rabdioph  26207  dvdsrabdioph  26214  fphpd  26222  monotuz  26349  oddcomabszz  26352  fnwe2lem3  26472  flcidc  26702  sumsnd  27020  csbafv12g  27325  csbaovg  27368  fargshiftfva  27762  cdlemk54  31216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-sbc 3068  df-csb 3158
  Copyright terms: Public domain W3C validator