This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcbr

Description: Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018)

Ref Expression
Assertion sbcbr ( [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 )

Proof

Step Hyp Ref Expression
1 sbcbr123 ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
2 csbconstg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 )
3 csbconstg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐶 )
4 2 3 breq12d ⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 ) )
5 br0 ⊢ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
6 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ∅ )
7 6 breqd ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
8 5 7 mtbiri ⊢ ( ¬ 𝐴 ∈ V → ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
9 br0 ⊢ ¬ 𝐵 ∅ 𝐶
10 6 breqd ⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 ↔ 𝐵 ∅ 𝐶 ) )
11 9 10 mtbiri ⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 )
12 8 11 2falsed ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 ) )
13 4 12 pm2.61i ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 )
14 1 13 bitri ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 𝐶 )