Theorem csbeq1 3143

Description: Analog of dfsbcq 3046 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 3046	. . 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 3141	. 2 |- [_ A / x ]_ C = { y | [. A / x ]. y e. C }
4		df-csb 3141	. 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 3044   [_csb 3140

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 3045  df-csb 3141

This theorem is referenced by:  csbeq1d  3147  csbeq1a  3149  csbiebg  3183  sbcnestgf  3192  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  csbing  3430  disjnims  4102  sbcbrg  4166  csbopabg  4190  pofun  4435  csbima12g  5125  csbiotag  5347  fvmpts  5757  fvmpt2  5763  mptfvex  5765  elfvmptrab1  5774  fmptcof  5846  fmptcos  5847  fliftfuns  5973  csbriotag  6019  riotaeqimp  6030  csbov123g  6091  elovmporab1w  6257  eqerlem  6800  qliftfuns  6855  summodclem2a  12075  zsumdc  12078  fsum3  12081  sumsnf  12103  sumsns  12109  fsum2dlemstep  12128  fisumcom2  12132  fsumshftm  12139  fisum0diag2  12141  fsumiun  12171  prodsnf  12286  fprodm1s  12295  fprodp1s  12296  prodsns  12297  fprod2dlemstep  12316  fprodcom2fi  12320  pcmptdvds  13051  ctiunctlemf  13210  mulcncflem  15521  fsumdvdsmul  15908