Theorem csbeq1 3438

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   {cab 2452   [.wsbc 3331   [_csb 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sbc 3332  df-csb 3436

This theorem is referenced by:  csbeq1d  3442  csbeq1a  3444  csbiebg  3458  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  sbcnestgf  3839  csbun  3857  csbin  3860  csbingOLD  3861  csbif  3989  csbifgOLD  3990  disjors  4433  disjxiun  4444  sbcbr123  4498  sbcbrgOLD  4499  csbopab  4779  csbopabgALT  4780  pofun  4816  csbima12  5354  csbima12gOLD  5355  csbiota  5580  csbiotagOLD  5581  fvmpts  5952  fvmpt2i  5956  fvmptex  5960  elfvmptrab1  5970  fmptcof  6055  fmptcos  6056  fliftfuns  6200  csbriota  6257  csbov123  6315  csbovgOLD  6317  elovmpt2rab1  6506  mpt2sn  6874  mpt2curryvald  6999  fvmpt2curryd  7000  eqerlem  7343  qliftfuns  7398  boxcutc  7512  iunfi  7808  wdom2d  8006  summolem2a  13500  zsum  13503  fsum  13505  sumsn  13526  sumsns  13528  fsum2dlem  13548  fsumcom2  13552  fsumshftm  13559  fsum0diag2  13561  fsumrlim  13588  fsumo1  13589  fsumiun  13598  pcmptdvds  14272  gsummpt1n0  16795  telgsumfzslem  16820  telgsumfzs  16821  psrass1lem  17828  coe1fzgsumdlem  18142  gsummoncoe1  18145  evl1gsumdlem  18191  madugsum  18940  fiuncmp  19698  elmptrab  20091  ovolfiniun  21675  finiunmbl  21717  volfiniun  21720  iundisj  21721  iundisj2  21722  iunmbl  21726  itgfsum  21996  dvfsumle  22185  dvfsumabs  22187  dvfsumlem2  22191  dvfsumlem3  22192  dvfsumlem4  22193  dvfsum2  22198  itgsubstlem  22212  itgsubst  22213  rlimcnp2  23052  fsumdvdscom  23217  fsumdvdsmul  23227  fsumvma  23244  dchrisumlem2  23431  fargshiftfva  24343  ifeqeqx  27121  disji2f  27139  disjorsf  27142  disjif2  27143  disjabrex  27144  disjabrexf  27145  disjxpin  27148  iundisjf  27149  iundisj2f  27150  disjunsn  27154  fvmpt2f  27198  funcnv4mpt  27212  iundisjfi  27297  iundisj2fi  27298  gsummpt2co  27462  prodmolem2a  28671  prodsn  28697  fprodm1s  28704  fprodp1s  28705  prodsns  28706  fprod2dlem  28715  fprodcom2  28719  finixpnum  29643  csbeq12  30198  mzpsubst  30313  rabdiophlem2  30367  elnn0rabdioph  30368  dvdsrabdioph  30375  fphpd  30382  monotuz  30509  oddcomabszz  30512  fnwe2lem3  30630  flcidc  30756  sumsnd  31007  fourierdlem103  31538  fourierdlem104  31539  csbafv12g  31717  csbaovg  31760  fsumshftd  33772  fsumshftdOLD  33773  cdlemk54  35772