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

Metamath Proof Explorer

Theorem sbcbr123

Description: Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005) (Revised by NM, 22-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 sbcex ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 → 𝐴 ∈ V )
2 br0 ⊢ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
3 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ∅ )
4 3 breqd ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
5 2 4 mtbiri ⊢ ( ¬ 𝐴 ∈ V → ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
6 5 con4i ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 → 𝐴 ∈ V )
7 dfsbcq2 ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 ) )
8 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
9 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝑅 = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 )
10 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
11 8 9 10 breq123d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
12 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
13 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑅
14 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
15 12 13 14 nfbr ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
16 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
17 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝑅 = ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
18 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
19 16 17 18 breq123d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 𝑅 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
20 15 19 sbiev ⊢ ( [ 𝑦 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
21 7 11 20 vtoclbg ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
22 1 6 21 pm5.21nii ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 𝑅 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )