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	syl5bb	|- ( 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	syl5eq	|- ( S e. V -> [_ S / x ]_ Word x = Word S )