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  11943  zsumdc  11946  fsum3  11949  sumsnf  11971  sumsns  11977  fsum2dlemstep  11996  fisumcom2  12000  fsumshftm  12007  fisum0diag2  12009  fsumiun  12039  prodsnf  12154  fprodm1s  12163  fprodp1s  12164  prodsns  12165  fprod2dlemstep  12184  fprodcom2fi  12188  pcmptdvds  12919  ctiunctlemf  13060  mulcncflem  15333  fsumdvdsmul  15717