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 ⊢ [˙A / x]˙ B R C ↔ B ⦋ A / x⦌ R C

Proof

Step Hyp Ref Expression
1 sbcbr123 ⊢ [˙A / x]˙ B R C ↔ ⦋ A / x⦌ B ⦋ A / x⦌ R ⦋ A / x⦌ C
2 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ B = B
3 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ C = C
4 2 3 breq12d ⊢ A ∈ V → ⦋ A / x⦌ B ⦋ A / x⦌ R ⦋ A / x⦌ C ↔ B ⦋ A / x⦌ R C
5 br0 ⊢ ¬ ⦋ A / x⦌ B ∅ ⦋ A / x⦌ C
6 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ R = ∅
7 6 breqd ⊢ ¬ A ∈ V → ⦋ A / x⦌ B ⦋ A / x⦌ R ⦋ A / x⦌ C ↔ ⦋ A / x⦌ B ∅ ⦋ A / x⦌ C
8 5 7 mtbiri ⊢ ¬ A ∈ V → ¬ ⦋ A / x⦌ B ⦋ A / x⦌ R ⦋ A / x⦌ C
9 br0 ⊢ ¬ B ∅ C
10 6 breqd ⊢ ¬ A ∈ V → B ⦋ A / x⦌ R C ↔ B ∅ C
11 9 10 mtbiri ⊢ ¬ A ∈ V → ¬ B ⦋ A / x⦌ R C
12 8 11 2falsed ⊢ ¬ A ∈ V → ⦋ A / x⦌ B ⦋ A / x⦌ R ⦋ A / x⦌ C ↔ B ⦋ A / x⦌ R C
13 4 12 pm2.61i ⊢ ⦋ A / x⦌ B ⦋ A / x⦌ R ⦋ A / x⦌ C ↔ B ⦋ A / x⦌ R C
14 1 13 bitri ⊢ [˙A / x]˙ B R C ↔ B ⦋ A / x⦌ R C