Theorem csbeq1 3144

Description: Analog of dfsbcq 3047 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 3047	. . 3 |- ( A = B -> ( [. A / x ]. y e. C <-> [. B / x ]. y e. C ) )
2	1	abbidv 2354	. 2 |- ( A = B -> { y | [. A / x ]. y e. C } = { y | [. B / x ]. y e. C } )
3		df-csb 3142	. 2 |- [_ A / x ]_ C = { y | [. A / x ]. y e. C }
4		df-csb 3142	. 2 |- [_ B / x ]_ C = { y | [. B / x ]. y e. C }
5	2, 3, 4	3eqtr4g 2292	1 |- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205   {cab 2220   [.wsbc 3045   [_csb 3141

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-sbc 3046  df-csb 3142

This theorem is referenced by:  csbeq1d  3148  csbeq1a  3150  csbiebg  3184  sbcnestgf  3193  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  csbing  3432  ifeqeqxdc  3673  disjnims  4105  sbcbrg  4169  csbopabg  4193  pofun  4438  csbima12g  5128  csbiotag  5350  fvmpts  5760  fvmpt2  5766  mptfvex  5768  elfvmptrab1  5777  fmptcof  5849  fmptcos  5850  fliftfuns  5977  csbriotag  6025  riotaeqimp  6036  csbov123g  6097  elovmporab1w  6263  eqerlem  6811  qliftfuns  6866  summodclem2a  12095  zsumdc  12098  fsum3  12101  sumsnf  12123  sumsns  12129  fsum2dlemstep  12148  fisumcom2  12152  fsumshftm  12159  fisum0diag2  12161  fsumiun  12191  prodsnf  12306  fprodm1s  12315  fprodp1s  12316  prodsns  12317  fprod2dlemstep  12336  fprodcom2fi  12340  pcmptdvds  13071  ctiunctlemf  13276  mulcncflem  15601  fsumdvdsmul  15988