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

Theorem csbid 3438
Description: Analog of sbid 1997 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbid  |-  [_ x  /  x ]_ A  =  A

Proof of Theorem csbid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-csb 3431 . 2  |-  [_ x  /  x ]_ A  =  { y  |  [. x  /  x ]. y  e.  A }
2 sbcid 3344 . . 3  |-  ( [. x  /  x ]. y  e.  A  <->  y  e.  A
)
32abbii 2591 . 2  |-  { y  |  [. x  /  x ]. y  e.  A }  =  { y  |  y  e.  A }
4 abid2 2597 . 2  |-  { y  |  y  e.  A }  =  A
51, 3, 43eqtri 2490 1  |-  [_ x  /  x ]_ A  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    e. wcel 1819   {cab 2442   [.wsbc 3327   [_csb 3430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328  df-csb 3431
This theorem is referenced by:  csbeq1a  3439  fvmpt2i  5963  fvmpt2curryd  7018  gsummoncoe1  18473  gsumply1eq  18474  disji2f  27577  disjif2  27581  disjabrex  27582  disjabrexf  27583  fvmpt2f  27647  gsummpt2co  27931  measiuns  28361  fphpd  30954  fsumsplitf  31771  dvmptmulf  31937
  Copyright terms: Public domain W3C validator