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

Theorem csbid 3873
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 3861 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3761 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2807 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2876 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2769 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {cab 2714  [wsbc 3744  csb 3860
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-sbc 3745  df-csb 3861
This theorem is referenced by:  csbeq1a  3874  fvmpt2f  6954  fvmpt2i  6963  fvmpocurryd  8207  fsumsplitf  15634  gsummoncoe1  21691  gsumply1eq  21692  disji2f  31537  disjif2  31541  disjabrex  31542  disjabrexf  31543  gsummpt2co  31932  measiuns  32856  fphpd  41168  disjrnmpt2  43481  climinf2mpt  44029  climinfmpt  44030  dvmptmulf  44252  sge0f1o  44697
  Copyright terms: Public domain W3C validator