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 e. _V -> [_ A / x ]_ B = B )
3 csbconstg 
 |-  ( A e. _V -> [_ A / x ]_ C = C )
4 2 3 breq12d 
 |-  ( A e. _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 e. _V -> [_ A / x ]_ R = (/) )
7 6 breqd 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C <-> [_ A / x ]_ B (/) [_ A / x ]_ C ) )
8 5 7 mtbiri 
 |-  ( -. A e. _V -> -. [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C )
9 br0 
 |-  -. B (/) C
10 6 breqd 
 |-  ( -. A e. _V -> ( B [_ A / x ]_ R C <-> B (/) C ) )
11 9 10 mtbiri 
 |-  ( -. A e. _V -> -. B [_ A / x ]_ R C )
12 8 11 2falsed 
 |-  ( -. A e. _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 )