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 ∈ V → ⦋ S / x⦌ Word x = Word S

Proof

Step Hyp Ref Expression
1 df-word ⊢ Word x = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x
2 1 csbeq2i ⊢ ⦋ S / x⦌ Word x = ⦋ S / x⦌ w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x
3 sbcrex ⊢ [˙S / x]˙ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x ↔ ∃ l ∈ ℕ 0 [˙S / x]˙ w : 0 ..^ l ⟶ x
4 sbcfg ⊢ S ∈ V → [˙S / x]˙ w : 0 ..^ l ⟶ x ↔ ⦋ S / x⦌ w : ⦋ S / x⦌ 0 ..^ l ⟶ ⦋ S / x⦌ x
5 csbconstg ⊢ S ∈ V → ⦋ S / x⦌ w = w
6 csbconstg ⊢ S ∈ V → ⦋ S / x⦌ 0 ..^ l = 0 ..^ l
7 csbvarg ⊢ S ∈ V → ⦋ S / x⦌ x = S
8 5 6 7 feq123d ⊢ S ∈ V → ⦋ S / x⦌ w : ⦋ S / x⦌ 0 ..^ l ⟶ ⦋ S / x⦌ x ↔ w : 0 ..^ l ⟶ S
9 4 8 bitrd ⊢ S ∈ V → [˙S / x]˙ w : 0 ..^ l ⟶ x ↔ w : 0 ..^ l ⟶ S
10 9 rexbidv ⊢ S ∈ V → ∃ l ∈ ℕ 0 [˙S / x]˙ w : 0 ..^ l ⟶ x ↔ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
11 3 10 bitrid ⊢ S ∈ V → [˙S / x]˙ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x ↔ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
12 11 abbidv ⊢ S ∈ V → w | [˙S / x]˙ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
13 csbab ⊢ ⦋ S / x⦌ w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x = w | [˙S / x]˙ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x
14 df-word ⊢ Word S = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
15 12 13 14 3eqtr4g ⊢ S ∈ V → ⦋ S / x⦌ w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ x = Word S
16 2 15 eqtrid ⊢ S ∈ V → ⦋ S / x⦌ Word x = Word S