Theorem csbeq1 3437

Description: Analog of dfsbcq 3329 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1

Proof of Theorem csbeq1

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq 3329	. . 3
2	1	abbidv 2593	. 2
3		df-csb 3435	. 2
4		df-csb 3435	. 2
5	2, 3, 4	3eqtr4g 2523	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  {cab 2442  [.wsbc 3327  [_csb 3434

This theorem is referenced by:  csbeq1d  3441  csbeq1a  3443  csbiebg  3457  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  sbcnestgf  3839  csbun  3857  csbin  3860  csbingOLD  3861  csbif  3991  csbifgOLD  3992  disjors  4438  disjxiun  4449  sbcbr123  4503  sbcbrgOLD  4504  csbopab  4784  csbopabgALT  4785  pofun  4821  csbima12  5359  csbima12gOLD  5360  csbiota  5585  csbiotagOLD  5586  fvmpts  5958  fvmpt2i  5962  fvmptex  5966  elfvmptrab1  5976  fmptcof  6065  fmptcos  6066  fliftfuns  6212  csbriota  6269  csbov123  6330  csbovgOLD  6332  elovmpt2rab1  6522  mpt2sn  6891  mpt2curryvald  7018  fvmpt2curryd  7019  eqerlem  7362  qliftfuns  7417  boxcutc  7532  iunfi  7828  wdom2d  8027  summolem2a  13537  zsum  13540  fsum  13542  sumsn  13563  sumsns  13565  fsum2dlem  13585  fsumcom2  13589  fsumshftm  13596  fsum0diag2  13598  fsumrlim  13625  fsumo1  13626  fsumiun  13635  prodmolem2a  13741  prodsn  13767  fprodm1s  13774  fprodp1s  13775  prodsns  13776  fprod2dlem  13784  fprodcom2  13788  pcmptdvds  14413  gsummpt1n0  16992  telgsumfzslem  17017  telgsumfzs  17018  psrass1lem  18029  coe1fzgsumdlem  18343  gsummoncoe1  18346  evl1gsumdlem  18392  madugsum  19145  fiuncmp  19904  elmptrab  20328  ovolfiniun  21912  finiunmbl  21954  volfiniun  21957  iundisj  21958  iundisj2  21959  iunmbl  21963  itgfsum  22233  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsum2  22435  itgsubstlem  22449  itgsubst  22450  rlimcnp2  23296  fsumdvdscom  23461  fsumdvdsmul  23471  fsumvma  23488  dchrisumlem2  23675  fargshiftfva  24639  ifeqeqx  27419  disji2f  27438  disjorsf  27441  disjif2  27442  disjabrex  27443  disjabrexf  27444  disjxpin  27447  iundisjf  27448  iundisj2f  27449  disjunsn  27453  fvmpt2f  27498  funcnv4mpt  27512  iundisjfi  27601  iundisj2fi  27602  finixpnum  30038  csbeq12  30566  mzpsubst  30681  rabdiophlem2  30735  elnn0rabdioph  30736  dvdsrabdioph  30743  fphpd  30750  monotuz  30877  oddcomabszz  30880  fnwe2lem3  30998  flcidc  31123  sumsnd  31401  sumsnf  31570  prodsnf  31587  dvnmptdivc  31735  fourierdlem103  31992  fourierdlem104  31993  csbafv12g  32222  csbaovg  32265  fsumshftd  34682  fsumshftdOLD  34683  cdlemk54  36684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328  df-csb 3435