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

Theorem csbid 3442
 Description: Analog of sbid 1996 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbid

Proof of Theorem csbid
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-csb 3435 . 2
2 sbcid 3344 . . 3
32abbii 2591 . 2
4 abid2 2597 . 2
51, 3, 43eqtri 2490 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  e.wcel 1818  {cab 2442  [.wsbc 3327  [_csb 3434 This theorem is referenced by:  csbeq1a  3443  fvmpt2i  5962  fvmpt2curryd  7019  gsummoncoe1  18346  gsumply1eq  18347  disji2f  27438  disjif2  27442  disjabrex  27443  disjabrexf  27444  fvmpt2f  27498  gsummpt2co  27771  measiuns  28188  fphpd  30750  fsumsplitf  31568  dvmptmulf  31734 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
 Copyright terms: Public domain W3C validator