Theorem csbeq1 3129

Description: Analog of dfsbcq 3032 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.

Step	Hyp	Ref	Expression
1		dfsbcq 3032	. . 3 |- ( A = B -> ( [. A / x ]. y e. C <-> [. B / x ]. y e. C ) )
2	1	abbidv 2348	. 2 |- ( A = B -> { y | [. A / x ]. y e. C } = { y | [. B / x ]. y e. C } )
3		df-csb 3127	. 2 |- [_ A / x ]_ C = { y | [. A / x ]. y e. C }
4		df-csb 3127	. 2 |- [_ B / x ]_ C = { y | [. B / x ]. y e. C }
5	2, 3, 4	3eqtr4g 2288	1 |- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2201   {cab 2216   [.wsbc 3030   [_csb 3126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-sbc 3031  df-csb 3127

This theorem is referenced by:  csbeq1d  3133  csbeq1a  3135  csbiebg  3169  sbcnestgf  3178  cbvralcsf  3189  cbvrexcsf  3190  cbvreucsf  3191  cbvrabcsf  3192  csbing  3413  disjnims  4080  sbcbrg  4144  csbopabg  4168  pofun  4411  csbima12g  5099  csbiotag  5321  fvmpts  5727  fvmpt2  5733  mptfvex  5735  elfvmptrab1  5744  fmptcof  5817  fmptcos  5818  fliftfuns  5944  csbriotag  5990  riotaeqimp  6001  csbov123g  6062  elovmporab1w  6228  eqerlem  6738  qliftfuns  6793  summodclem2a  11965  zsumdc  11968  fsum3  11971  sumsnf  11993  sumsns  11999  fsum2dlemstep  12018  fisumcom2  12022  fsumshftm  12029  fisum0diag2  12031  fsumiun  12061  prodsnf  12176  fprodm1s  12185  fprodp1s  12186  prodsns  12187  fprod2dlemstep  12206  fprodcom2fi  12210  pcmptdvds  12941  ctiunctlemf  13082  mulcncflem  15360  fsumdvdsmul  15744