Metamath Proof Explorer

Theorem sbcbr1g

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

Ref Expression
Assertion sbcbr1g 
|- ( A e. V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R 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 ]_ C = C )
3 2 breq2d 
 |-  ( A e. V -> ( [_ A / x ]_ B R [_ A / x ]_ C <-> [_ A / x ]_ B R C ) )
4 1 3 bitrd 
 |-  ( A e. V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R C ) )