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 )`