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

Theorem csbid 3911
Description: Analogue of sbid 2254 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 3899 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3804 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2808 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2878 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2768 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2107  {cab 2713  [wsbc 3787  csb 3898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-sbc 3788  df-csb 3899
This theorem is referenced by:  csbeq1a  3912  fvmpt2f  7016  fvmpt2i  7025  fvmpocurryd  8297  fsumsplitf  15779  gsummoncoe1  22313  gsumply1eq  22314  disji2f  32591  disjif2  32595  disjabrex  32596  disjabrexf  32597  gsummpt2co  33052  measiuns  34219  fphpd  42832  disjrnmpt2  45198  climinf2mpt  45734  climinfmpt  45735  dvmptmulf  45957  sge0f1o  46402
  Copyright terms: Public domain W3C validator