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

Theorem csbvarg 3843
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 3117 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vex 3111 . . . . . 6  |-  y  e. 
_V
3 df-csb 3431 . . . . . . 7  |-  [_ y  /  x ]_ x  =  { z  |  [. y  /  x ]. z  e.  x }
4 sbcel2gv 3393 . . . . . . . 8  |-  ( y  e.  _V  ->  ( [. y  /  x ]. z  e.  x  <->  z  e.  y ) )
54abbi1dv 2600 . . . . . . 7  |-  ( y  e.  _V  ->  { z  |  [. y  /  x ]. z  e.  x }  =  y )
63, 5syl5eq 2515 . . . . . 6  |-  ( y  e.  _V  ->  [_ y  /  x ]_ x  =  y )
72, 6ax-mp 5 . . . . 5  |-  [_ y  /  x ]_ x  =  y
87csbeq2i 3831 . . . 4  |-  [_ A  /  y ]_ [_ y  /  x ]_ x  = 
[_ A  /  y ]_ y
9 csbco 3440 . . . 4  |-  [_ A  /  y ]_ [_ y  /  x ]_ x  = 
[_ A  /  x ]_ x
10 df-csb 3431 . . . 4  |-  [_ A  /  y ]_ y  =  { z  |  [. A  /  y ]. z  e.  y }
118, 9, 103eqtr3i 2499 . . 3  |-  [_ A  /  x ]_ x  =  { z  |  [. A  /  y ]. z  e.  y }
12 sbcel2gv 3393 . . . 4  |-  ( A  e.  _V  ->  ( [. A  /  y ]. z  e.  y  <->  z  e.  A ) )
1312abbi1dv 2600 . . 3  |-  ( A  e.  _V  ->  { z  |  [. A  / 
y ]. z  e.  y }  =  A )
1411, 13syl5eq 2515 . 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 1374    e. wcel 1762   {cab 2447   _Vcvv 3108   [.wsbc 3326   [_csb 3430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3110  df-sbc 3327  df-csb 3431
This theorem is referenced by:  sbccsb2  3846  sbccsb2gOLD  3847  csbfv  5897  csbfvgOLD  5898  ixpsnval  7464  csbwrdg  12525  swrdspsleq  12625  telgsums  16808  ixpsnbasval  17633  scmatscm  18777  pm2mpf1lem  19057  pm2mpcoe1  19063  idpm2idmp  19064  pm2mpmhmlem2  19082  monmat2matmon  19087  pm2mp  19088  fvmptnn04if  19112  chfacfscmulfsupp  19122  cayhamlem4  19151  nbgraopALT  24088  rusgrasn  24609  iuninc  27089  f1od2  27207  csbvargi  30113  rusbcALT  30881  divcncf  31179  ply1mulgsumlem4  31939  onfrALTlem5  32271  onfrALTlem4  32272  onfrALTlem5VD  32642  onfrALTlem4VD  32643  bnj110  32872  bj-sels  33478  renegclALT  33643  cdlemk40  35590
  Copyright terms: Public domain W3C validator