MPE Home 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  6177  fvmpt2i  6184  fvmpt2curryd  7262  gsummoncoe1  19444  gsumply1eq  19445  disji2f  28566  disjif2  28570  disjabrex  28571  disjabrexf  28572  gsummpt2co  28905  measiuns  29401  fphpd  36192  disjrnmpt2  38164  fsumsplitf  38428  dvmptmulf  38621  sge0f1o  39069
  Copyright terms: Public domain W3C validator