Metamath Proof Explorer

Theorem csbov123

Description: Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbov123 ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) )
2 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ 𝐹 )
3 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
5 2 3 4 oveq123d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
6 1 5 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
7 vex ⊢ 𝑦 ∈ V
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐹
10 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
11 8 9 10 nfov ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
12 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐹 = ⦋ 𝑦 / 𝑥 ⦌ 𝐹 )
13 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
15 12 13 14 oveq123d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
16 7 11 15 csbief ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝐹 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
17 6 16 vtoclg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
18 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ∅ )
19 df-ov ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ⟩ )
20 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ∅ )
21 20 fveq1d ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ⟩ ) = ( ∅ ‘ ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ⟩ ) )
22 0fv ⊢ ( ∅ ‘ ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ⟩ ) = ∅
23 21 22 eqtrdi ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ⟩ ) = ∅ )
24 19 23 eqtr2id ⊢ ( ¬ 𝐴 ∈ V → ∅ = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
25 18 24 eqtrd ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
26 17 25 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )