Theorem csbeq1 3140

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203   {cab 2218   [.wsbc 3041   [_csb 3137

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-sbc 3042  df-csb 3138

This theorem is referenced by:  csbeq1d  3144  csbeq1a  3146  csbiebg  3180  sbcnestgf  3189  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  csbing  3427  disjnims  4099  sbcbrg  4163  csbopabg  4187  pofun  4432  csbima12g  5122  csbiotag  5344  fvmpts  5754  fvmpt2  5760  mptfvex  5762  elfvmptrab1  5771  fmptcof  5843  fmptcos  5844  fliftfuns  5970  csbriotag  6016  riotaeqimp  6027  csbov123g  6088  elovmporab1w  6254  eqerlem  6797  qliftfuns  6852  summodclem2a  12060  zsumdc  12063  fsum3  12066  sumsnf  12088  sumsns  12094  fsum2dlemstep  12113  fisumcom2  12117  fsumshftm  12124  fisum0diag2  12126  fsumiun  12156  prodsnf  12271  fprodm1s  12280  fprodp1s  12281  prodsns  12282  fprod2dlemstep  12301  fprodcom2fi  12305  pcmptdvds  13036  ctiunctlemf  13178  mulcncflem  15459  fsumdvdsmul  15846