Theorem csbeq1 3378

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

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   {cab 2448   [.wsbc 3279   [_csb 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-sbc 3280  df-csb 3376

This theorem is referenced by:  csbeq1d  3382  csbeq1a  3384  csbiebg  3398  cbvralcsf  3407  cbvreucsf  3409  cbvrabcsf  3410  sbcnestgf  3796  csbun  3810  csbin  3811  csbif  3943  disjors  4402  disjxiun  4413  sbcbr123  4468  csbopab  4747  csbopabgALT  4748  pofun  4790  csbima12  5204  csbima12gOLD  5205  csbiota  5594  fvmpt2f  5972  fvmpts  5974  fvmpt2i  5979  fvmptex  5983  elfvmptrab1  5993  fmptcof  6081  fmptcos  6082  fliftfuns  6232  csbriota  6289  csbov123  6349  elovmpt2rab1  6543  mpt2sn  6914  mpt2curryvald  7043  fvmpt2curryd  7044  eqerlem  7421  qliftfuns  7476  boxcutc  7591  iunfi  7888  wdom2d  8121  summolem2a  13830  zsum  13833  fsum  13835  sumsn  13856  sumsns  13860  fsum2dlem  13880  fsumcom2  13884  fsumshftm  13891  fsum0diag2  13893  fsumrlim  13920  fsumo1  13921  fsumiun  13930  prodmolem2a  14037  prodsn  14065  prodsnf  14067  fprodm1s  14073  fprodp1s  14074  prodsns  14075  fprod2dlem  14083  fprodcom2  14087  pcmptdvds  14888  gsummpt1n0  17646  telgsumfzslem  17667  telgsumfzs  17668  psrass1lem  18650  coe1fzgsumdlem  18944  gsummoncoe1  18947  evl1gsumdlem  18993  madugsum  19717  fiuncmp  20468  elmptrab  20891  ovolfiniun  22503  finiunmbl  22546  volfiniun  22549  iundisj  22550  iundisj2  22551  iunmbl  22555  itgfsum  22833  dvfsumle  23022  dvfsumabs  23024  dvfsumlem2  23028  dvfsumlem3  23029  dvfsumlem4  23030  dvfsum2  23035  itgsubstlem  23049  itgsubst  23050  rlimcnp2  23941  fsumdvdscom  24163  fsumdvdsmul  24173  fsumvma  24190  dchrisumlem2  24377  fargshiftfva  25416  ifeqeqx  28207  disji2f  28236  disjorsf  28239  disjif2  28240  disjabrex  28241  disjabrexf  28242  disjxpin  28247  iundisjf  28248  iundisj2f  28249  disjunsn  28253  aciunf1lem  28313  funcnv4mpt  28322  iundisjfi  28421  iundisj2fi  28422  gsummpt2co  28592  csbdif  31771  finixpnum  31975  poimirlem24  32009  poimirlem26  32011  csbeq12  32446  fsumshftd  32568  fsumshftdOLD  32569  cdlemk54  34570  mzpsubst  35635  rabdiophlem2  35690  elnn0rabdioph  35691  dvdsrabdioph  35698  fphpd  35704  monotuz  35834  oddcomabszz  35837  fnwe2lem3  35955  flcidc  36085  csbcog  36286  csbingOLD  37255  sumsnd  37387  disjf1  37495  disjrnmpt2  37501  sumsnf  37686  dvnmptdivc  37851  fourierdlem103  38111  fourierdlem104  38112  csbafv12g  38677  csbaovg  38720  riotaeqimp  39079