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

Theorem csbid 3905
Description: Analogue of sbid 2248 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 3893 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3793 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2803 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2872 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2765 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {cab 2710  [wsbc 3776  csb 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3777  df-csb 3893
This theorem is referenced by:  csbeq1a  3906  fvmpt2f  6995  fvmpt2i  7004  fvmpocurryd  8251  fsumsplitf  15684  gsummoncoe1  21810  gsumply1eq  21811  disji2f  31786  disjif2  31790  disjabrex  31791  disjabrexf  31792  gsummpt2co  32178  measiuns  33153  fphpd  41487  disjrnmpt2  43819  climinf2mpt  44365  climinfmpt  44366  dvmptmulf  44588  sge0f1o  45033
  Copyright terms: Public domain W3C validator