Theorem csbeq1 3536

Description: Analogue of dfsbcq 3437 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 3437	. . 3 |- ( A = B -> ( [. A / x ]. y e. C <-> [. B / x ]. y e. C ) )
2	1	abbidv 2741	. 2 |- ( A = B -> { y | [. A / x ]. y e. C } = { y | [. B / x ]. y e. C } )
3		df-csb 3534	. 2 |- [_ A / x ]_ C = { y | [. A / x ]. y e. C }
4		df-csb 3534	. 2 |- [_ B / x ]_ C = { y | [. B / x ]. y e. C }
5	2, 3, 4	3eqtr4g 2681	1 |- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   {cab 2608   [.wsbc 3435   [_csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436  df-csb 3534

This theorem is referenced by:  csbeq1d  3540  csbeq1a  3542  csbiebg  3556  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  sbcnestgf  3995  csbun  4009  csbin  4010  csbif  4138  disjors  4635  disjxiun  4649  disjxiunOLD  4650  sbcbr123  4706  csbopab  5008  csbopabgALT  5009  pofun  5051  csbima12  5483  csbiota  5881  fvmpt2f  6283  fvmpts  6285  fvmpt2i  6290  fvmptex  6294  elfvmptrab1  6305  fmptcof  6397  fmptcos  6398  fliftfuns  6564  csbriota  6623  riotaeqimp  6634  csbov123  6687  elovmpt2rab1  6881  el2mpt2csbcl  7250  mpt2sn  7268  mpt2curryvald  7396  fvmpt2curryd  7397  eqerlem  7776  qliftfuns  7834  boxcutc  7951  iunfi  8254  wdom2d  8485  summolem2a  14446  zsum  14449  fsum  14451  sumsnf  14473  sumsn  14475  sumsns  14479  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsum0diag2  14515  fsumrlim  14543  fsumo1  14544  fsumiun  14553  prodmolem2a  14664  prodsn  14692  prodsnf  14694  fprodm1s  14700  fprodp1s  14701  prodsns  14702  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  pcmptdvds  15598  gsummpt1n0  18364  telgsumfzslem  18385  telgsumfzs  18386  psrass1lem  19377  coe1fzgsumdlem  19671  gsummoncoe1  19674  evl1gsumdlem  19720  madugsum  20449  fiuncmp  21207  elmptrab  21630  ovolfiniun  23269  finiunmbl  23312  volfiniun  23315  iundisj  23316  iundisj2  23317  iunmbl  23321  itgfsum  23593  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  itgsubstlem  23811  itgsubst  23812  rlimcnp2  24693  fsumdvdscom  24911  fsumdvdsmul  24921  fsumvma  24938  dchrisumlem2  25179  ifeqeqx  29361  disji2f  29390  disjorsf  29393  disjif2  29394  disjabrex  29395  disjabrexf  29396  disjxpin  29401  iundisjf  29402  iundisj2f  29403  disjunsn  29407  aciunf1lem  29462  funcnv4mpt  29470  iundisjfi  29555  iundisj2fi  29556  fsumiunle  29575  gsummpt2co  29780  csbdif  33171  finixpnum  33394  poimirlem24  33433  poimirlem26  33435  csbeq12  33966  fsumshftd  34237  fsumshftdOLD  34238  cdlemk54  36246  mzpsubst  37311  rabdiophlem2  37366  elnn0rabdioph  37367  dvdsrabdioph  37374  fphpd  37380  monotuz  37506  oddcomabszz  37509  fnwe2lem3  37622  flcidc  37744  csbcog  37941  csbingOLD  39054  sumsnd  39185  disjf1  39369  disjrnmpt2  39375  climinf2mpt  39946  climinfmpt  39947  dvnmptdivc  40153  fourierdlem103  40426  fourierdlem104  40427  csbafv12g  41217  csbaovg  41260  fargshiftfva  41379