Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbvarg Unicode version

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.
StepHypRef Expression
1 elex 3118 . 2
2 vex 3112 . . . . . 6
3 df-csb 3435 . . . . . . 7
4 sbcel2gv 3394 . . . . . . . 8
54abbi1dv 2595 . . . . . . 7
63, 5syl5eq 2510 . . . . . 6
72, 6ax-mp 5 . . . . 5
87csbeq2i 3836 . . . 4
9 csbco 3444 . . . 4
10 df-csb 3435 . . . 4
118, 9, 103eqtr3i 2494 . . 3
12 sbcel2gv 3394 . . . 4
1312abbi1dv 2595 . . 3
1411, 13syl5eq 2510 . 2
151, 14syl 16 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator