This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbvarg

Description: The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005)

Ref Expression
Assertion csbvarg 
|- ( A e. V -> [_ A / x ]_ x = A )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 df-csb 
 |-  [_ y / x ]_ x = { z | [. y / x ]. z e. x }
3 sbcel2gv 
 |-  ( y e. _V -> ( [. y / x ]. z e. x <-> z e. y ) )
4 3 eqabcdv 
 |-  ( y e. _V -> { z | [. y / x ]. z e. x } = y )
5 2 4 eqtrid 
 |-  ( y e. _V -> [_ y / x ]_ x = y )
6 5 elv 
 |-  [_ y / x ]_ x = y
7 6 csbeq2i 
 |-  [_ A / y ]_ [_ y / x ]_ x = [_ A / y ]_ y
8 csbcow 
 |-  [_ A / y ]_ [_ y / x ]_ x = [_ A / x ]_ x
9 df-csb 
 |-  [_ A / y ]_ y = { z | [. A / y ]. z e. y }
10 7 8 9 3eqtr3i 
 |-  [_ A / x ]_ x = { z | [. A / y ]. z e. y }
11 sbcel2gv 
 |-  ( A e. _V -> ( [. A / y ]. z e. y <-> z e. A ) )
12 11 eqabcdv 
 |-  ( A e. _V -> { z | [. A / y ]. z e. y } = A )
13 10 12 eqtrid 
 |-  ( A e. _V -> [_ A / x ]_ x = A )
14 1 13 syl 
 |-  ( A e. V -> [_ A / x ]_ x = A )