Theorem csbaovg

Description: Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	csbaovg	⊢ ( 𝐴 ∈ 𝐷 → ⦋ 𝐴 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) = (( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )) )

Proof

Step	Hyp	Ref	Expression
1		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) = ⦋ 𝐴 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) )
2		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ 𝐹 )
3		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
5	2 3 4	aoveq123d	⊢ ( 𝑦 = 𝐴 → (( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )) = (( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )) )
6	1 5	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) = (( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )) ↔ ⦋ 𝐴 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) = (( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )) ) )
7		vex	⊢ 𝑦 ∈ V
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐹
10		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
11	8 9 10	nfaov	⊢ Ⅎ 𝑥 (( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ))
12		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐹 = ⦋ 𝑦 / 𝑥 ⦌ 𝐹 )
13		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
15	12 13 14	aoveq123d	⊢ ( 𝑥 = 𝑦 → (( 𝐵 𝐹 𝐶 )) = (( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )) )
16	7 11 15	csbief	⊢ ⦋ 𝑦 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) = (( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ))
17	6 16	vtoclg	⊢ ( 𝐴 ∈ 𝐷 → ⦋ 𝐴 / 𝑥 ⦌ (( 𝐵 𝐹 𝐶 )) = (( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )) )