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

Theorem csbid 3373
Description: Analogue of sbid 2088 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 3366 . 2  |-  [_ x  /  x ]_ A  =  { y  |  [. x  /  x ]. y  e.  A }
2 sbcid 3286 . . 3  |-  ( [. x  /  x ]. y  e.  A  <->  y  e.  A
)
32abbii 2569 . 2  |-  { y  |  [. x  /  x ]. y  e.  A }  =  { y  |  y  e.  A }
4 abid2 2575 . 2  |-  { y  |  y  e.  A }  =  A
51, 3, 43eqtri 2479 1  |-  [_ x  /  x ]_ A  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1446    e. wcel 1889   {cab 2439   [.wsbc 3269   [_csb 3365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3270  df-csb 3366
This theorem is referenced by:  csbeq1a  3374  fvmpt2f  5954  fvmpt2i  5961  fvmpt2curryd  7023  gsummoncoe1  18910  gsumply1eq  18911  disji2f  28199  disjif2  28203  disjabrex  28204  disjabrexf  28205  gsummpt2co  28555  measiuns  29051  fphpd  35671  disjrnmpt2  37473  fsumsplitf  37656  dvmptmulf  37822  sge0f1o  38234
  Copyright terms: Public domain W3C validator