Metamath Proof Explorer

Theorem sbcrel

Description: Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion sbcrel 
|- ( A e. V -> ( [. A / x ]. Rel R <-> Rel [_ A / x ]_ R ) )

Proof

Step Hyp Ref Expression
1 sbcssg 
 |-  ( A e. V -> ( [. A / x ]. R C_ ( _V X. _V ) <-> [_ A / x ]_ R C_ [_ A / x ]_ ( _V X. _V ) ) )
2 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ ( _V X. _V ) = ( _V X. _V ) )
3 2 sseq2d 
 |-  ( A e. V -> ( [_ A / x ]_ R C_ [_ A / x ]_ ( _V X. _V ) <-> [_ A / x ]_ R C_ ( _V X. _V ) ) )
4 1 3 bitrd 
 |-  ( A e. V -> ( [. A / x ]. R C_ ( _V X. _V ) <-> [_ A / x ]_ R C_ ( _V X. _V ) ) )
5 df-rel 
 |-  ( Rel R <-> R C_ ( _V X. _V ) )
6 5 sbcbii 
 |-  ( [. A / x ]. Rel R <-> [. A / x ]. R C_ ( _V X. _V ) )
7 df-rel 
 |-  ( Rel [_ A / x ]_ R <-> [_ A / x ]_ R C_ ( _V X. _V ) )
8 4 6 7 3bitr4g 
 |-  ( A e. V -> ( [. A / x ]. Rel R <-> Rel [_ A / x ]_ R ) )