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

Theorem csbvarg 3798
Description: The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbvarg  |-  ( A  e.  V  ->  [_ A  /  x ]_ x  =  A )

Proof of Theorem csbvarg
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3077 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vex 3071 . . . . . 6  |-  y  e. 
_V
3 df-csb 3387 . . . . . . 7  |-  [_ y  /  x ]_ x  =  { z  |  [. y  /  x ]. z  e.  x }
4 sbcel2gv 3351 . . . . . . . 8  |-  ( y  e.  _V  ->  ( [. y  /  x ]. z  e.  x  <->  z  e.  y ) )
54abbi1dv 2589 . . . . . . 7  |-  ( y  e.  _V  ->  { z  |  [. y  /  x ]. z  e.  x }  =  y )
63, 5syl5eq 2504 . . . . . 6  |-  ( y  e.  _V  ->  [_ y  /  x ]_ x  =  y )
72, 6ax-mp 5 . . . . 5  |-  [_ y  /  x ]_ x  =  y
87csbeq2i 3786 . . . 4  |-  [_ A  /  y ]_ [_ y  /  x ]_ x  = 
[_ A  /  y ]_ y
9 csbco 3396 . . . 4  |-  [_ A  /  y ]_ [_ y  /  x ]_ x  = 
[_ A  /  x ]_ x
10 df-csb 3387 . . . 4  |-  [_ A  /  y ]_ y  =  { z  |  [. A  /  y ]. z  e.  y }
118, 9, 103eqtr3i 2488 . . 3  |-  [_ A  /  x ]_ x  =  { z  |  [. A  /  y ]. z  e.  y }
12 sbcel2gv 3351 . . . 4  |-  ( A  e.  _V  ->  ( [. A  /  y ]. z  e.  y  <->  z  e.  A ) )
1312abbi1dv 2589 . . 3  |-  ( A  e.  _V  ->  { z  |  [. A  / 
y ]. z  e.  y }  =  A )
1411, 13syl5eq 2504 . 2  |-  ( A  e.  _V  ->  [_ A  /  x ]_ x  =  A )
151, 14syl 16 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ x  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   {cab 2436   _Vcvv 3068   [.wsbc 3284   [_csb 3386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3070  df-sbc 3285  df-csb 3387
This theorem is referenced by:  sbccsb2  3801  sbccsb2gOLD  3802  csbfv  5827  csbfvgOLD  5828  ixpsnval  7366  csbwrdg  12359  swrdspsleq  12444  ixpsnbasval  17396  iuninc  26045  f1od2  26158  csbvargi  29062  rusbcALT  29831  rusgrasn  30695  telescgsum  30955  ply1mulgsumlem4  30989  pmatcollpw1aa0  31235  pmattomply1f1lem  31255  pmattomply1coe1  31259  idpmattoidmply1  31260  pmattomply1mhmlem1  31273  pmattomply1mhmlem2  31274  monmat2matmon  31278  pmat2matp  31279  fvmptnn04if  31303  chfacfscmulfsupp  31313  cayhamlem4  31343  onfrALTlem5  31550  onfrALTlem4  31551  onfrALTlem5VD  31921  onfrALTlem4VD  31922  bnj110  32151  bj-sels  32755  renegclALT  32920  cdlemk40  34867
  Copyright terms: Public domain W3C validator