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

Theorem csbeq1 3084
Description: Analog of dfsbcq 2993 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 2993 . . 3  |-  ( A  =  B  ->  ( [. A  /  x ]. y  e.  C  <->  [. B  /  x ]. y  e.  C )
)
21abbidv 2397 . 2  |-  ( A  =  B  ->  { y  |  [. A  /  x ]. y  e.  C }  =  { y  |  [. B  /  x ]. y  e.  C } )
3 df-csb 3082 . 2  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
4 df-csb 3082 . 2  |-  [_ B  /  x ]_ C  =  { y  |  [. B  /  x ]. y  e.  C }
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   {cab 2269   [.wsbc 2991   [_csb 3081
This theorem is referenced by:  csbeq1d  3087  csbeq1a  3089  csbiebg  3120  sbcnestgf  3128  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  csbing  3376  csbifg  3593  disjors  4009  disjxiun  4020  sbcbrg  4072  csbopabg  4094  pofun  4330  csbima12g  5022  csbiotag  5248  fvmpts  5603  fvmpt2i  5607  fvmptex  5610  fmptcof  5692  fmptcos  5693  fliftfuns  5813  csbovg  5889  csbriotag  6317  eqerlem  6692  qliftfuns  6745  boxcutc  6859  iunfi  7144  wdom2d  7294  summolem2a  12188  sumsn  12213  sumsns  12215  fsum2dlem  12233  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  fsumrlim  12269  fsumo1  12270  fsumiun  12279  pcmptdvds  12942  psrass1lem  16123  fiuncmp  17131  elmptrab  17522  ovolfiniun  18860  finiunmbl  18901  volfiniun  18904  iundisj  18905  iundisj2  18906  iunmbl  18910  itgfsum  19181  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsum2  19381  itgsubstlem  19395  itgsubst  19396  rlimcnp2  20261  fsumdvdscom  20425  fsumdvdsmul  20435  fsumvma  20452  dchrisumlem2  20639  ifeqeqx  23034  fvmpt2f  23224  funcnv4mpt  23237  disji2f  23354  disjorsf  23357  disjif2  23358  disjabrex  23359  disjabrexf  23360  iundisjfi  23363  iundisj2fi  23364  iundisjf  23365  iundisj2f  23366  fprod1s  25325  fprodp1s  25327  mzpsubst  26826  rabdiophlem2  26883  elnn0rabdioph  26884  dvdsrabdioph  26891  fphpd  26899  monotuz  27026  oddcomabszz  27029  fnwe2lem3  27149  flcidc  27379  sumsnd  27697  csbafv12g  28000  csbaovg  28040  cdlemk54  31147
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator