Theorem csbeq1 3312

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   {cab 2429   [.wsbc 3207   [_csb 3309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-sbc 3208  df-csb 3310

This theorem is referenced by:  csbeq1d  3316  csbeq1a  3318  csbiebg  3332  cbvralcsf  3340  cbvreucsf  3342  cbvrabcsf  3343  sbcnestgf  3712  csbun  3730  csbin  3733  csbingOLD  3734  csbif  3860  csbifgOLD  3861  disjors  4299  disjxiun  4310  sbcbr123  4364  sbcbrgOLD  4365  csbopab  4641  csbopabgALT  4642  pofun  4678  csbima12  5207  csbima12gOLD  5208  csbiota  5431  csbiotagOLD  5432  fvmpts  5797  fvmpt2i  5801  fvmptex  5805  fmptcof  5898  fmptcos  5899  fliftfuns  6028  csbriota  6085  csbov123  6143  csbovgOLD  6145  mpt2curryvald  6810  fvmpt2curryd  6811  eqerlem  7154  qliftfuns  7208  boxcutc  7327  iunfi  7620  wdom2d  7816  summolem2a  13213  zsum  13216  fsum  13218  sumsn  13238  sumsns  13240  fsum2dlem  13258  fsumcom2  13262  fsumshftm  13269  fsum0diag2  13271  fsumrlim  13295  fsumo1  13296  fsumiun  13305  pcmptdvds  13977  gsummpt1n0  16478  psrass1lem  17469  evl1gsumdlem  17812  madugsum  18471  fiuncmp  19029  elmptrab  19422  ovolfiniun  21006  finiunmbl  21047  volfiniun  21050  iundisj  21051  iundisj2  21052  iunmbl  21056  itgfsum  21326  dvfsumle  21515  dvfsumabs  21517  dvfsumlem2  21521  dvfsumlem3  21522  dvfsumlem4  21523  dvfsum2  21528  itgsubstlem  21542  itgsubst  21543  rlimcnp2  22382  fsumdvdscom  22547  fsumdvdsmul  22557  fsumvma  22574  dchrisumlem2  22761  fargshiftfva  23547  ifeqeqx  25924  disji2f  25943  disjorsf  25946  disjif2  25947  disjabrex  25948  disjabrexf  25949  disjxpin  25952  iundisjf  25953  iundisj2f  25954  disjunsn  25958  fvmpt2f  25997  funcnv4mpt  26011  iundisjfi  26102  iundisj2fi  26103  gsummpt2co  26271  prodmolem2a  27469  prodsn  27495  fprodm1s  27502  fprodp1s  27503  prodsns  27504  fprod2dlem  27513  fprodcom2  27517  finixpnum  28440  csbeq12  28996  mzpsubst  29111  rabdiophlem2  29166  elnn0rabdioph  29167  dvdsrabdioph  29174  fphpd  29181  monotuz  29308  oddcomabszz  29311  fnwe2lem3  29431  flcidc  29557  sumsnd  29774  csbafv12g  30069  csbaovg  30112  elfvmptrab1  30180  elovmpt2rab1  30185  mpt2sn  30750  telescfzgsumlem  30842  telescfzgsum  30843  coe1fzgsumdlem  30870  gsummoncoe1  30876  fsumshftd  32698  fsumshftdOLD  32699  cdlemk54  34698