Metamath Proof Explorer

Theorem csbov

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

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

Proof

Step Hyp Ref Expression
1 csbov123 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
2 csbconstg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 )
3 csbconstg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐶 )
4 2 3 oveq12d ⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) )
5 0fv ⊢ ( ∅ ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = ∅
6 df-ov ⊢ ( 𝐵 ∅ 𝐶 ) = ( ∅ ‘ ⟨ 𝐵 , 𝐶 ⟩ )
7 0ov ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ∅
8 5 6 7 3eqtr4ri ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ∅ 𝐶 )
9 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ∅ )
10 9 oveqd ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
11 9 oveqd ⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) = ( 𝐵 ∅ 𝐶 ) )
12 8 10 11 3eqtr4a ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) )
13 4 12 pm2.61i ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 )
14 1 13 eqtri ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 )