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

Theorem csbid 3682
Description: Analogue of sbid 2261 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 3675 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3593 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2877 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2883 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2786 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2139  {cab 2746  [wsbc 3576  csb 3674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-sbc 3577  df-csb 3675
This theorem is referenced by:  csbeq1a  3683  fvmpt2f  6446  fvmpt2i  6453  fvmpt2curryd  7567  fsumsplitf  14691  gsummoncoe1  19896  gsumply1eq  19897  disji2f  29718  disjif2  29722  disjabrex  29723  disjabrexf  29724  gsummpt2co  30110  measiuns  30610  fphpd  37900  disjrnmpt2  39892  climinf2mpt  40467  climinfmpt  40468  dvmptmulf  40673  sge0f1o  41120
  Copyright terms: Public domain W3C validator