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 
|- ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 sbcex 
 |-  ( [. A / x ]. B R C -> A e. _V )
2 br0 
 |-  -. [_ A / x ]_ B (/) [_ A / x ]_ C
3 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ R = (/) )
4 3 breqd 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C <-> [_ A / x ]_ B (/) [_ A / x ]_ C ) )
5 2 4 mtbiri 
 |-  ( -. A e. _V -> -. [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C )
6 5 con4i 
 |-  ( [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C -> A e. _V )
7 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] B R C <-> [. A / x ]. B R C ) )
8 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
9 csbeq1 
 |-  ( y = A -> [_ y / x ]_ R = [_ A / x ]_ R )
10 csbeq1 
 |-  ( y = A -> [_ y / x ]_ C = [_ A / x ]_ C )
11 8 9 10 breq123d 
 |-  ( y = A -> ( [_ y / x ]_ B [_ y / x ]_ R [_ y / x ]_ C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C ) )
12 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
13 nfcsb1v 
 |-  F/_ x [_ y / x ]_ R
14 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
15 12 13 14 nfbr 
 |-  F/ x [_ y / x ]_ B [_ y / x ]_ R [_ y / x ]_ C
16 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
17 csbeq1a 
 |-  ( x = y -> R = [_ y / x ]_ R )
18 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
19 16 17 18 breq123d 
 |-  ( x = y -> ( B R C <-> [_ y / x ]_ B [_ y / x ]_ R [_ y / x ]_ C ) )
20 15 19 sbiev 
 |-  ( [ y / x ] B R C <-> [_ y / x ]_ B [_ y / x ]_ R [_ y / x ]_ C )
21 7 11 20 vtoclbg 
 |-  ( A e. _V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C ) )
22 1 6 21 pm5.21nii 
 |-  ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C )