Theorem csbeq1 3130

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202   {cab 2217   [.wsbc 3031   [_csb 3127

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-sbc 3032  df-csb 3128

This theorem is referenced by:  csbeq1d  3134  csbeq1a  3136  csbiebg  3170  sbcnestgf  3179  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  csbing  3414  disjnims  4079  sbcbrg  4143  csbopabg  4167  pofun  4409  csbima12g  5097  csbiotag  5319  fvmpts  5724  fvmpt2  5730  mptfvex  5732  elfvmptrab1  5741  fmptcof  5814  fmptcos  5815  fliftfuns  5939  csbriotag  5985  riotaeqimp  5996  csbov123g  6057  elovmporab1w  6223  eqerlem  6733  qliftfuns  6788  summodclem2a  11944  zsumdc  11947  fsum3  11950  sumsnf  11972  sumsns  11978  fsum2dlemstep  11997  fisumcom2  12001  fsumshftm  12008  fisum0diag2  12010  fsumiun  12040  prodsnf  12155  fprodm1s  12164  fprodp1s  12165  prodsns  12166  fprod2dlemstep  12185  fprodcom2fi  12189  pcmptdvds  12920  ctiunctlemf  13061  mulcncflem  15334  fsumdvdsmul  15718