Theorem csbeq1 3279

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755   {cab 2419   [.wsbc 3175   [_csb 3276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-sbc 3176  df-csb 3277

This theorem is referenced by:  csbeq1d  3283  csbeq1a  3285  csbiebg  3299  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  sbcnestgf  3679  csbun  3697  csbin  3700  csbingOLD  3701  csbif  3827  csbifgOLD  3828  disjors  4266  disjxiun  4277  sbcbr123  4331  sbcbrgOLD  4332  csbopab  4609  csbopabgOLD  4610  pofun  4644  csbima12  5174  csbima12gOLD  5175  csbiota  5398  csbiotagOLD  5399  fvmpts  5764  fvmpt2i  5768  fvmptex  5772  fmptcof  5864  fmptcos  5865  fliftfuns  5994  csbriota  6052  csbov123  6111  csbovgOLD  6113  eqerlem  7121  qliftfuns  7175  boxcutc  7294  iunfi  7587  wdom2d  7783  summolem2a  13175  zsum  13178  fsum  13180  sumsn  13200  sumsns  13202  fsum2dlem  13220  fsumcom2  13224  fsumshftm  13230  fsum0diag2  13232  fsumrlim  13256  fsumo1  13257  fsumiun  13266  pcmptdvds  13938  psrass1lem  17380  madugsum  18290  fiuncmp  18848  elmptrab  19241  ovolfiniun  20825  finiunmbl  20866  volfiniun  20869  iundisj  20870  iundisj2  20871  iunmbl  20875  itgfsum  21145  dvfsumle  21334  dvfsumabs  21336  dvfsumlem2  21340  dvfsumlem3  21341  dvfsumlem4  21342  dvfsum2  21347  itgsubstlem  21361  itgsubst  21362  rlimcnp2  22244  fsumdvdscom  22409  fsumdvdsmul  22419  fsumvma  22436  dchrisumlem2  22623  fargshiftfva  23347  ifeqeqx  25725  disji2f  25744  disjorsf  25747  disjif2  25748  disjabrex  25749  disjabrexf  25750  disjxpin  25753  iundisjf  25754  iundisj2f  25755  disjunsn  25759  fvmpt2f  25798  funcnv4mpt  25812  iundisjfi  25902  iundisj2fi  25903  gsummpt2co  26100  prodmolem2a  27293  prodsn  27319  fprodm1s  27326  fprodp1s  27327  prodsns  27328  fprod2dlem  27337  fprodcom2  27341  finixpnum  28255  csbeq12  28811  mzpsubst  28927  rabdiophlem2  28982  elnn0rabdioph  28983  dvdsrabdioph  28990  fphpd  28997  monotuz  29124  oddcomabszz  29127  fnwe2lem3  29247  flcidc  29373  sumsnd  29590  csbafv12g  29886  csbaovg  29929  elfvmptrab1  29997  elovmpt2rab1  30002  mpt2sn  30565  cdlemk54  34172