Theorem csbeq1 3107

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

Syntax hints:   -> wi 4   = wceq 1375   e. wcel 2180   {cab 2195   [.wsbc 3008   [_csb 3104

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-sbc 3009  df-csb 3105

This theorem is referenced by:  csbeq1d  3111  csbeq1a  3113  csbiebg  3147  sbcnestgf  3156  cbvralcsf  3167  cbvrexcsf  3168  cbvreucsf  3169  cbvrabcsf  3170  csbing  3391  disjnims  4053  sbcbrg  4117  csbopabg  4141  pofun  4380  csbima12g  5065  csbiotag  5287  fvmpts  5685  fvmpt2  5691  mptfvex  5693  elfvmptrab1  5702  fmptcof  5775  fmptcos  5776  fliftfuns  5895  csbriotag  5941  riotaeqimp  5952  csbov123g  6013  elovmporab1w  6177  eqerlem  6681  qliftfuns  6736  summodclem2a  11858  zsumdc  11861  fsum3  11864  sumsnf  11886  sumsns  11892  fsum2dlemstep  11911  fisumcom2  11915  fsumshftm  11922  fisum0diag2  11924  fsumiun  11954  prodsnf  12069  fprodm1s  12078  fprodp1s  12079  prodsns  12080  fprod2dlemstep  12099  fprodcom2fi  12103  pcmptdvds  12834  ctiunctlemf  12975  mulcncflem  15246  fsumdvdsmul  15630