Metamath Proof Explorer

Theorem sbcbr2g

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

Ref Expression
Assertion sbcbr2g 
|- ( A e. V -> ( [. A / x ]. B R C <-> B R [_ A / x ]_ C ) )

Proof

Step Hyp Ref Expression
1 sbcbr12g 
 |-  ( A e. V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R [_ A / x ]_ C ) )
2 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ B = B )
3 2 breq1d 
 |-  ( A e. V -> ( [_ A / x ]_ B R [_ A / x ]_ C <-> B R [_ A / x ]_ C ) )
4 1 3 bitrd 
 |-  ( A e. V -> ( [. A / x ]. B R C <-> B R [_ A / x ]_ C ) )