Theorem csbeq1 3214

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721   {cab 2390   [.wsbc 3121   [_csb 3211

This theorem is referenced by:  csbeq1d  3217  csbeq1a  3219  csbiebg  3250  sbcnestgf  3258  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  csbing  3508  csbifg  3727  disjors  4158  disjxiun  4169  sbcbrg  4221  csbopabg  4243  pofun  4479  csbima12g  5172  csbiotag  5406  fvmpts  5766  fvmpt2i  5770  fvmptex  5774  fmptcof  5861  fmptcos  5862  fliftfuns  5995  csbovg  6071  csbriotag  6521  eqerlem  6896  qliftfuns  6950  boxcutc  7064  iunfi  7353  wdom2d  7504  summolem2a  12464  sumsn  12489  sumsns  12491  fsum2dlem  12509  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  fsumrlim  12545  fsumo1  12546  fsumiun  12555  pcmptdvds  13218  psrass1lem  16397  fiuncmp  17421  elmptrab  17812  ovolfiniun  19350  finiunmbl  19391  volfiniun  19394  iundisj  19395  iundisj2  19396  iunmbl  19400  itgfsum  19671  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsum2  19871  itgsubstlem  19885  itgsubst  19886  rlimcnp2  20758  fsumdvdscom  20923  fsumdvdsmul  20933  fsumvma  20950  dchrisumlem2  21137  fargshiftfva  21579  ifeqeqx  23954  disji2f  23972  disjorsf  23975  disjif2  23976  disjabrex  23977  disjabrexf  23978  disjxpin  23981  iundisjf  23982  iundisj2f  23983  fvmpt2f  24025  funcnv4mpt  24038  iundisjfi  24105  iundisj2fi  24106  prodmolem2a  25213  prodsn  25239  fprodm1s  25246  fprodp1s  25247  prodsns  25248  fprod2dlem  25257  fprodcom2  25261  mzpsubst  26695  rabdiophlem2  26752  elnn0rabdioph  26753  dvdsrabdioph  26760  fphpd  26767  monotuz  26894  oddcomabszz  26897  fnwe2lem3  27017  flcidc  27247  sumsnd  27564  csbafv12g  27868  csbaovg  27911  cdlemk54  31440

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-sbc 3122  df-csb 3212