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

Theorem csbvarg 3834
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 3104 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vex 3098 . . . . . 6  |-  y  e. 
_V
3 df-csb 3421 . . . . . . 7  |-  [_ y  /  x ]_ x  =  { z  |  [. y  /  x ]. z  e.  x }
4 sbcel2gv 3380 . . . . . . . 8  |-  ( y  e.  _V  ->  ( [. y  /  x ]. z  e.  x  <->  z  e.  y ) )
54abbi1dv 2581 . . . . . . 7  |-  ( y  e.  _V  ->  { z  |  [. y  /  x ]. z  e.  x }  =  y )
63, 5syl5eq 2496 . . . . . 6  |-  ( y  e.  _V  ->  [_ y  /  x ]_ x  =  y )
72, 6ax-mp 5 . . . . 5  |-  [_ y  /  x ]_ x  =  y
87csbeq2i 3822 . . . 4  |-  [_ A  /  y ]_ [_ y  /  x ]_ x  = 
[_ A  /  y ]_ y
9 csbco 3430 . . . 4  |-  [_ A  /  y ]_ [_ y  /  x ]_ x  = 
[_ A  /  x ]_ x
10 df-csb 3421 . . . 4  |-  [_ A  /  y ]_ y  =  { z  |  [. A  /  y ]. z  e.  y }
118, 9, 103eqtr3i 2480 . . 3  |-  [_ A  /  x ]_ x  =  { z  |  [. A  /  y ]. z  e.  y }
12 sbcel2gv 3380 . . . 4  |-  ( A  e.  _V  ->  ( [. A  /  y ]. z  e.  y  <->  z  e.  A ) )
1312abbi1dv 2581 . . 3  |-  ( A  e.  _V  ->  { z  |  [. A  / 
y ]. z  e.  y }  =  A )
1411, 13syl5eq 2496 . 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 1383    e. wcel 1804   {cab 2428   _Vcvv 3095   [.wsbc 3313   [_csb 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-sbc 3314  df-csb 3421
This theorem is referenced by:  sbccsb2  3837  sbccsb2gOLD  3838  csbfv  5894  csbfvgOLD  5895  ixpsnval  7474  csbwrdg  12549  swrdspsleq  12652  telgsums  16896  ixpsnbasval  17729  scmatscm  18888  pm2mpf1lem  19168  pm2mpcoe1  19174  idpm2idmp  19175  pm2mpmhmlem2  19193  monmat2matmon  19198  pm2mp  19199  fvmptnn04if  19223  chfacfscmulfsupp  19233  cayhamlem4  19262  nbgraopALT  24296  rusgrasn  24817  iuninc  27300  f1od2  27419  csbvargi  30496  rusbcALT  31300  divcncf  31593  ply1mulgsumlem4  32724  onfrALTlem5  33047  onfrALTlem4  33048  onfrALTlem5VD  33418  onfrALTlem4VD  33419  bnj110  33649  bj-sels  34268  renegclALT  34434  cdlemk40  36383
  Copyright terms: Public domain W3C validator