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

Theorem csbid 3823
Description: Analogue of sbid 2220 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 3812 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3723 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2861 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2926 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2823 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1522  wcel 2081  {cab 2775  [wsbc 3706  csb 3811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1525  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-sbc 3707  df-csb 3812
This theorem is referenced by:  csbeq1a  3824  fvmpt2f  6636  fvmpt2i  6644  fvmpocurryd  7788  fsumsplitf  14931  gsummoncoe1  20155  gsumply1eq  20156  disji2f  30017  disjif2  30021  disjabrex  30022  disjabrexf  30023  gsummpt2co  30495  measiuns  31093  fphpd  38898  disjrnmpt2  40989  climinf2mpt  41537  climinfmpt  41538  dvmptmulf  41763  sge0f1o  42206
  Copyright terms: Public domain W3C validator