Theorem csbeq1 3420

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

Syntax hints:   -> wi 4   = wceq 1381   e. wcel 1802   {cab 2426   [.wsbc 3311   [_csb 3417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-sbc 3312  df-csb 3418

This theorem is referenced by:  csbeq1d  3424  csbeq1a  3426  csbiebg  3440  cbvralcsf  3449  cbvreucsf  3451  cbvrabcsf  3452  sbcnestgf  3821  csbun  3839  csbin  3842  csbingOLD  3843  csbif  3972  csbifgOLD  3973  disjors  4419  disjxiun  4430  sbcbr123  4484  sbcbrgOLD  4485  csbopab  4765  csbopabgALT  4766  pofun  4802  csbima12  5340  csbima12gOLD  5341  csbiota  5566  csbiotagOLD  5567  fvmpts  5939  fvmpt2i  5943  fvmptex  5947  elfvmptrab1  5957  fmptcof  6046  fmptcos  6047  fliftfuns  6193  csbriota  6250  csbov123  6311  csbovgOLD  6313  elovmpt2rab1  6503  mpt2sn  6872  mpt2curryvald  6997  fvmpt2curryd  6998  eqerlem  7341  qliftfuns  7396  boxcutc  7510  iunfi  7806  wdom2d  8004  summolem2a  13511  zsum  13514  fsum  13516  sumsn  13537  sumsns  13539  fsum2dlem  13559  fsumcom2  13563  fsumshftm  13570  fsum0diag2  13572  fsumrlim  13599  fsumo1  13600  fsumiun  13609  pcmptdvds  14285  gsummpt1n0  16861  telgsumfzslem  16886  telgsumfzs  16887  psrass1lem  17897  coe1fzgsumdlem  18211  gsummoncoe1  18214  evl1gsumdlem  18260  madugsum  19012  fiuncmp  19770  elmptrab  20194  ovolfiniun  21778  finiunmbl  21820  volfiniun  21823  iundisj  21824  iundisj2  21825  iunmbl  21829  itgfsum  22099  dvfsumle  22288  dvfsumabs  22290  dvfsumlem2  22294  dvfsumlem3  22295  dvfsumlem4  22296  dvfsum2  22301  itgsubstlem  22315  itgsubst  22316  rlimcnp2  23161  fsumdvdscom  23326  fsumdvdsmul  23336  fsumvma  23353  dchrisumlem2  23540  fargshiftfva  24504  ifeqeqx  27284  disji2f  27303  disjorsf  27306  disjif2  27307  disjabrex  27308  disjabrexf  27309  disjxpin  27312  iundisjf  27313  iundisj2f  27314  disjunsn  27318  fvmpt2f  27363  funcnv4mpt  27377  iundisjfi  27466  iundisj2fi  27467  prodmolem2a  29034  prodsn  29060  fprodm1s  29067  fprodp1s  29068  prodsns  29069  fprod2dlem  29078  fprodcom2  29082  finixpnum  30006  csbeq12  30534  mzpsubst  30649  rabdiophlem2  30703  elnn0rabdioph  30704  dvdsrabdioph  30711  fphpd  30718  monotuz  30845  oddcomabszz  30848  fnwe2lem3  30966  flcidc  31092  sumsnd  31348  fourierdlem103  31877  fourierdlem104  31878  csbafv12g  32056  csbaovg  32099  fsumshftd  34384  fsumshftdOLD  34385  cdlemk54  36386