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

Theorem csbid 3736
Description: Analogue of sbid 2282 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 3729 . 2 𝑥 / 𝑥𝐴 = {𝑦[𝑥 / 𝑥]𝑦𝐴}
2 sbcid 3650 . . 3 ([𝑥 / 𝑥]𝑦𝐴𝑦𝐴)
32abbii 2923 . 2 {𝑦[𝑥 / 𝑥]𝑦𝐴} = {𝑦𝑦𝐴}
4 abid2 2929 . 2 {𝑦𝑦𝐴} = 𝐴
51, 3, 43eqtri 2832 1 𝑥 / 𝑥𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2156  {cab 2792  [wsbc 3633  csb 3728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-sbc 3634  df-csb 3729
This theorem is referenced by:  csbeq1a  3737  fvmpt2f  6504  fvmpt2i  6511  fvmpt2curryd  7632  fsumsplitf  14695  gsummoncoe1  19882  gsumply1eq  19883  disji2f  29715  disjif2  29719  disjabrex  29720  disjabrexf  29721  gsummpt2co  30105  measiuns  30605  fphpd  37882  disjrnmpt2  39864  climinf2mpt  40426  climinfmpt  40427  dvmptmulf  40632  sge0f1o  41078
  Copyright terms: Public domain W3C validator