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

Theorem csbid 3574
Description: Analogue of sbid 2152 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 3567 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3485 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2768 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2774 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2677 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  {cab 2637  [wsbc 3468  csb 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sbc 3469  df-csb 3567
This theorem is referenced by:  csbeq1a  3575  fvmpt2f  6322  fvmpt2i  6329  fvmpt2curryd  7442  fsumsplitf  14516  gsummoncoe1  19722  gsumply1eq  19723  disji2f  29516  disjif2  29520  disjabrex  29521  disjabrexf  29522  gsummpt2co  29908  measiuns  30408  fphpd  37697  disjrnmpt2  39689  climinf2mpt  40264  climinfmpt  40265  dvmptmulf  40470  sge0f1o  40917
  Copyright terms: Public domain W3C validator