Theorem csbeq1 3423

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 1823   {cab 2439   [.wsbc 3324   [_csb 3420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325  df-csb 3421

This theorem is referenced by:  csbeq1d  3427  csbeq1a  3429  csbiebg  3443  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  sbcnestgf  3834  csbun  3848  csbin  3849  csbif  3979  disjors  4425  disjxiun  4436  sbcbr123  4490  csbopab  4768  csbopabgALT  4769  pofun  4805  csbima12  5342  csbima12gOLD  5343  csbiota  5563  fvmpts  5933  fvmpt2i  5938  fvmptex  5942  elfvmptrab1  5952  fmptcof  6041  fmptcos  6042  fliftfuns  6187  csbriota  6244  csbov123  6304  elovmpt2rab1  6495  mpt2sn  6864  mpt2curryvald  6991  fvmpt2curryd  6992  eqerlem  7335  qliftfuns  7390  boxcutc  7505  iunfi  7800  wdom2d  7998  summolem2a  13619  zsum  13622  fsum  13624  sumsn  13645  sumsns  13647  fsum2dlem  13667  fsumcom2  13671  fsumshftm  13678  fsum0diag2  13680  fsumrlim  13707  fsumo1  13708  fsumiun  13717  prodmolem2a  13823  prodsn  13849  fprodm1s  13856  fprodp1s  13857  prodsns  13858  fprod2dlem  13866  fprodcom2  13870  pcmptdvds  14497  gsummpt1n0  17188  telgsumfzslem  17212  telgsumfzs  17213  psrass1lem  18224  coe1fzgsumdlem  18538  gsummoncoe1  18541  evl1gsumdlem  18587  madugsum  19312  fiuncmp  20071  elmptrab  20494  ovolfiniun  22078  finiunmbl  22120  volfiniun  22123  iundisj  22124  iundisj2  22125  iunmbl  22129  itgfsum  22399  dvfsumle  22588  dvfsumabs  22590  dvfsumlem2  22594  dvfsumlem3  22595  dvfsumlem4  22596  dvfsum2  22601  itgsubstlem  22615  itgsubst  22616  rlimcnp2  23494  fsumdvdscom  23659  fsumdvdsmul  23669  fsumvma  23686  dchrisumlem2  23873  fargshiftfva  24841  ifeqeqx  27625  disji2f  27648  disjorsf  27651  disjif2  27652  disjabrex  27653  disjabrexf  27654  disjxpin  27658  iundisjf  27659  iundisj2f  27660  disjunsn  27664  fvmpt2f  27720  aciunf1lem  27729  funcnv4mpt  27739  iundisjfi  27835  iundisj2fi  27836  gsummpt2co  28005  finixpnum  30278  csbeq12  30806  mzpsubst  30920  rabdiophlem2  30975  elnn0rabdioph  30976  dvdsrabdioph  30983  fphpd  30989  monotuz  31116  oddcomabszz  31119  fnwe2lem3  31237  flcidc  31364  sumsnd  31641  sumsnf  31809  prodsnf  31826  dvnmptdivc  31974  fourierdlem103  32231  fourierdlem104  32232  csbafv12g  32461  csbaovg  32504  csbingOLD  34019  fsumshftd  35079  fsumshftdOLD  35080  cdlemk54  37081