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

Theorem csbid 3824
Description: Analogue of sbid 2253 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 3812 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3711 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2808 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2879 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2769 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2110  {cab 2714  [wsbc 3694  csb 3811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3695  df-csb 3812
This theorem is referenced by:  csbeq1a  3825  fvmpt2f  6819  fvmpt2i  6828  fvmpocurryd  8013  fsumsplitf  15306  gsummoncoe1  21225  gsumply1eq  21226  disji2f  30635  disjif2  30639  disjabrex  30640  disjabrexf  30641  gsummpt2co  31027  measiuns  31897  fphpd  40341  disjrnmpt2  42399  climinf2mpt  42930  climinfmpt  42931  dvmptmulf  43153  sge0f1o  43595
  Copyright terms: Public domain W3C validator