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

Theorem csbid 3507
 Description: Analogue of sbid 2100 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 3500 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3419 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2726 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2732 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2636 1 𝑥 / 𝑥𝐴 = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977  {cab 2596  [wsbc 3402  ⦋csb 3499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403  df-csb 3500 This theorem is referenced by:  csbeq1a  3508  fvmpt2f  6192  fvmpt2i  6199  fvmpt2curryd  7284  gsummoncoe1  19495  gsumply1eq  19496  disji2f  28772  disjif2  28776  disjabrex  28777  disjabrexf  28778  gsummpt2co  29111  measiuns  29607  fphpd  36398  disjrnmpt2  38370  fsumsplitf  38634  dvmptmulf  38827  sge0f1o  39275
 Copyright terms: Public domain W3C validator