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

Theorem csbid 3841
 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 3829 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3737 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2863 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2932 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2825 1 𝑥 / 𝑥𝐴 = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∈ wcel 2111  {cab 2776  [wsbc 3720  ⦋csb 3828 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721  df-csb 3829 This theorem is referenced by:  csbeq1a  3842  fvmpt2f  6746  fvmpt2i  6755  fvmpocurryd  7922  fsumsplitf  15092  gsummoncoe1  20940  gsumply1eq  20941  disji2f  30347  disjif2  30351  disjabrex  30352  disjabrexf  30353  gsummpt2co  30740  measiuns  31598  fphpd  39772  disjrnmpt2  41830  climinf2mpt  42371  climinfmpt  42372  dvmptmulf  42594  sge0f1o  43036
 Copyright terms: Public domain W3C validator