Theorem csbvarg 3848

Description: The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbvarg

Proof of Theorem csbvarg

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3118	. 2
2		vex 3112	. . . . . 6
3		df-csb 3435	. . . . . . 7
4		sbcel2gv 3394	. . . . . . . 8
5	4	abbi1dv 2595	. . . . . . 7
6	3, 5	syl5eq 2510	. . . . . 6
7	2, 6	ax-mp 5	. . . . 5
8	7	csbeq2i 3836	. . . 4
9		csbco 3444	. . . 4
10		df-csb 3435	. . . 4
11	8, 9, 10	3eqtr3i 2494	. . 3
12		sbcel2gv 3394	. . . 4
13	12	abbi1dv 2595	. . 3
14	11, 13	syl5eq 2510	. 2
15	1, 14	syl 16	1

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

This theorem is referenced by:  sbccsb2  3851  sbccsb2gOLD  3852  csbfv  5909  csbfvgOLD  5910  ixpsnval  7492  csbwrdg  12570  swrdspsleq  12673  telgsums  17022  ixpsnbasval  17855  scmatscm  19015  pm2mpf1lem  19295  pm2mpcoe1  19301  idpm2idmp  19302  pm2mpmhmlem2  19320  monmat2matmon  19325  pm2mp  19326  fvmptnn04if  19350  chfacfscmulfsupp  19360  cayhamlem4  19389  nbgraopALT  24424  rusgrasn  24945  iuninc  27428  f1od2  27547  csbvargi  30521  rusbcALT  31346  divcncf  31686  ply1mulgsumlem4  32989  onfrALTlem5  33314  onfrALTlem4  33315  onfrALTlem5VD  33685  onfrALTlem4VD  33686  bnj110  33916  bj-sels  34520  renegclALT  34694  cdlemk40  36643

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-or 370  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-v 3111  df-sbc 3328  df-csb 3435