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 𝐴 / 𝑥 ( 𝐵 𝐹 𝐶 ) = ( 𝐵 𝐴 / 𝑥 𝐹 𝐶 )