Theorem csbeq1 3395

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

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1867   {cab 2405   [.wsbc 3296   [_csb 3392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-sbc 3297  df-csb 3393

This theorem is referenced by:  csbeq1d  3399  csbeq1a  3401  csbiebg  3415  cbvralcsf  3424  cbvreucsf  3426  cbvrabcsf  3427  sbcnestgf  3809  csbun  3823  csbin  3824  csbif  3956  disjors  4403  disjxiun  4414  sbcbr123  4468  csbopab  4744  csbopabgALT  4745  pofun  4782  csbima12  5196  csbima12gOLD  5197  csbiota  5585  fvmpt2f  5956  fvmpts  5958  fvmpt2i  5963  fvmptex  5967  elfvmptrab1  5977  fmptcof  6063  fmptcos  6064  fliftfuns  6213  csbriota  6270  csbov123  6330  elovmpt2rab1  6521  mpt2sn  6889  mpt2curryvald  7016  fvmpt2curryd  7017  eqerlem  7394  qliftfuns  7449  boxcutc  7564  iunfi  7859  wdom2d  8086  summolem2a  13748  zsum  13751  fsum  13753  sumsn  13774  sumsns  13778  fsum2dlem  13798  fsumcom2  13802  fsumshftm  13809  fsum0diag2  13811  fsumrlim  13838  fsumo1  13839  fsumiun  13848  prodmolem2a  13955  prodsn  13983  prodsnf  13985  fprodm1s  13991  fprodp1s  13992  prodsns  13993  fprod2dlem  14001  fprodcom2  14005  pcmptdvds  14791  gsummpt1n0  17525  telgsumfzslem  17546  telgsumfzs  17547  psrass1lem  18529  coe1fzgsumdlem  18823  gsummoncoe1  18826  evl1gsumdlem  18872  madugsum  19592  fiuncmp  20343  elmptrab  20766  ovolfiniun  22328  finiunmbl  22371  volfiniun  22374  iundisj  22375  iundisj2  22376  iunmbl  22380  itgfsum  22658  dvfsumle  22847  dvfsumabs  22849  dvfsumlem2  22853  dvfsumlem3  22854  dvfsumlem4  22855  dvfsum2  22860  itgsubstlem  22874  itgsubst  22875  rlimcnp2  23754  fsumdvdscom  23974  fsumdvdsmul  23984  fsumvma  24001  dchrisumlem2  24188  fargshiftfva  25209  ifeqeqx  27994  disji2f  28023  disjorsf  28026  disjif2  28027  disjabrex  28028  disjabrexf  28029  disjxpin  28034  iundisjf  28035  iundisj2f  28036  disjunsn  28040  aciunf1lem  28101  funcnv4mpt  28110  iundisjfi  28205  iundisj2fi  28206  gsummpt2co  28378  csbdif  31467  finixpnum  31634  poimirlem24  31668  poimirlem26  31670  csbeq12  32105  fsumshftd  32232  fsumshftdOLD  32233  cdlemk54  34234  mzpsubst  35299  rabdiophlem2  35354  elnn0rabdioph  35355  dvdsrabdioph  35362  fphpd  35368  monotuz  35499  oddcomabszz  35502  fnwe2lem3  35620  flcidc  35743  csbcog  35884  csbingOLD  36859  sumsnd  36991  disjf1  37084  disjrnmpt2  37090  sumsnf  37227  dvnmptdivc  37386  fourierdlem103  37645  fourierdlem104  37646  csbafv12g  38042  csbaovg  38085