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

Metamath Proof Explorer

Theorem csbwrdg

Description: Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Assertion csbwrdg 
|- ( S e. V -> [_ S / x ]_ Word x = Word S )

Proof

Step Hyp Ref Expression
1 df-word 
 |-  Word x = { w | E. l e. NN0 w : ( 0 ..^ l ) --> x }
2 1 csbeq2i 
 |-  [_ S / x ]_ Word x = [_ S / x ]_ { w | E. l e. NN0 w : ( 0 ..^ l ) --> x }
3 sbcrex 
 |-  ( [. S / x ]. E. l e. NN0 w : ( 0 ..^ l ) --> x <-> E. l e. NN0 [. S / x ]. w : ( 0 ..^ l ) --> x )
4 sbcfg 
 |-  ( S e. V -> ( [. S / x ]. w : ( 0 ..^ l ) --> x <-> [_ S / x ]_ w : [_ S / x ]_ ( 0 ..^ l ) --> [_ S / x ]_ x ) )
5 csbconstg 
 |-  ( S e. V -> [_ S / x ]_ w = w )
6 csbconstg 
 |-  ( S e. V -> [_ S / x ]_ ( 0 ..^ l ) = ( 0 ..^ l ) )
7 csbvarg 
 |-  ( S e. V -> [_ S / x ]_ x = S )
8 5 6 7 feq123d 
 |-  ( S e. V -> ( [_ S / x ]_ w : [_ S / x ]_ ( 0 ..^ l ) --> [_ S / x ]_ x <-> w : ( 0 ..^ l ) --> S ) )
9 4 8 bitrd 
 |-  ( S e. V -> ( [. S / x ]. w : ( 0 ..^ l ) --> x <-> w : ( 0 ..^ l ) --> S ) )
10 9 rexbidv 
 |-  ( S e. V -> ( E. l e. NN0 [. S / x ]. w : ( 0 ..^ l ) --> x <-> E. l e. NN0 w : ( 0 ..^ l ) --> S ) )
11 3 10 bitrid 
 |-  ( S e. V -> ( [. S / x ]. E. l e. NN0 w : ( 0 ..^ l ) --> x <-> E. l e. NN0 w : ( 0 ..^ l ) --> S ) )
12 11 abbidv 
 |-  ( S e. V -> { w | [. S / x ]. E. l e. NN0 w : ( 0 ..^ l ) --> x } = { w | E. l e. NN0 w : ( 0 ..^ l ) --> S } )
13 csbab 
 |-  [_ S / x ]_ { w | E. l e. NN0 w : ( 0 ..^ l ) --> x } = { w | [. S / x ]. E. l e. NN0 w : ( 0 ..^ l ) --> x }
14 df-word 
 |-  Word S = { w | E. l e. NN0 w : ( 0 ..^ l ) --> S }
15 12 13 14 3eqtr4g 
 |-  ( S e. V -> [_ S / x ]_ { w | E. l e. NN0 w : ( 0 ..^ l ) --> x } = Word S )
16 2 15 eqtrid 
 |-  ( S e. V -> [_ S / x ]_ Word x = Word S )