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\in V\to ⦋S/x⦌\mathrm{Word}x=\mathrm{Word}S$$

Proof

Step	Hyp	Ref	Expression
1		df-word	$$⊢\mathrm{Word}x=\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\right\}$$
2	1	csbeq2i	$$⊢⦋S/x⦌\mathrm{Word}x=⦋S/x⦌\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\right\}$$
3		sbcrex	$$⊢\underset{\dot{}}{[}S/x\underset{\dot{}}{]}\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\leftrightarrow \exists l\in {\mathbb{N}}_0\underset{\dot{}}{[}S/x\underset{\dot{}}{]}w:\left(0..^l\right)⟶x$$
4		sbcfg	$$⊢S\in V\to \left(\underset{\dot{}}{[}S/x\underset{\dot{}}{]}w:\left(0..^l\right)⟶x\leftrightarrow ⦋S/x⦌w:⦋S/x⦌\left(0..^l\right)⟶⦋S/x⦌x\right)$$
5		csbconstg	$$⊢S\in V\to ⦋S/x⦌w=w$$
6		csbconstg	$$⊢S\in V\to ⦋S/x⦌\left(0..^l\right)=\left(0..^l\right)$$
7		csbvarg	$$⊢S\in V\to ⦋S/x⦌x=S$$
8	5 6 7	feq123d	$$⊢S\in V\to \left(⦋S/x⦌w:⦋S/x⦌\left(0..^l\right)⟶⦋S/x⦌x\leftrightarrow w:\left(0..^l\right)⟶S\right)$$
9	4 8	bitrd	$$⊢S\in V\to \left(\underset{\dot{}}{[}S/x\underset{\dot{}}{]}w:\left(0..^l\right)⟶x\leftrightarrow w:\left(0..^l\right)⟶S\right)$$
10	9	rexbidv	$$⊢S\in V\to \left(\exists l\in {\mathbb{N}}_0\underset{\dot{}}{[}S/x\underset{\dot{}}{]}w:\left(0..^l\right)⟶x\leftrightarrow \exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right)$$
11	3 10	syl5bb	$$⊢S\in V\to \left(\underset{\dot{}}{[}S/x\underset{\dot{}}{]}\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\leftrightarrow \exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right)$$
12	11	abbidv	$$⊢S\in V\to \left\{w|\underset{\dot{}}{[}S/x\underset{\dot{}}{]}\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\right\}=\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right\}$$
13		csbab	$$⊢⦋S/x⦌\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\right\}=\left\{w|\underset{\dot{}}{[}S/x\underset{\dot{}}{]}\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\right\}$$
14		df-word	$$⊢\mathrm{Word}S=\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right\}$$
15	12 13 14	3eqtr4g	$$⊢S\in V\to ⦋S/x⦌\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶x\right\}=\mathrm{Word}S$$
16	2 15	eqtrid	$$⊢S\in V\to ⦋S/x⦌\mathrm{Word}x=\mathrm{Word}S$$