Theorem csbeq1 3034

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

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128   {cab 2143   [.wsbc 2937   [_csb 3031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938  df-csb 3032

This theorem is referenced by:  csbeq1d  3038  csbeq1a  3040  csbiebg  3073  sbcnestgf  3082  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  csbing  3314  disjnims  3957  sbcbrg  4018  csbopabg  4042  pofun  4272  csbima12g  4946  csbiotag  5162  fvmpts  5545  fvmpt2  5550  mptfvex  5552  elfvmptrab1  5561  fmptcof  5633  fmptcos  5634  fliftfuns  5745  csbriotag  5789  csbov123g  5856  eqerlem  6508  qliftfuns  6561  summodclem2a  11273  zsumdc  11276  fsum3  11279  sumsnf  11301  sumsns  11307  fsum2dlemstep  11326  fisumcom2  11330  fsumshftm  11337  fisum0diag2  11339  fsumiun  11369  prodsnf  11484  fprodm1s  11493  fprodp1s  11494  prodsns  11495  fprod2dlemstep  11514  fprodcom2fi  11518  ctiunctlemf  12154  mulcncflem  12977