This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcco3gw

Description: Composition of two substitutions. Version of sbcco3g with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Nov-2005) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypothesis sbcco3gw.1 
|- ( x = A -> B = C )
Assertion sbcco3gw 
|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ph ) )

Proof

Step Hyp Ref Expression
1 sbcco3gw.1 
 |-  ( x = A -> B = C )
2 sbcnestgw 
 |-  ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
3 elex 
 |-  ( A e. V -> A e. _V )
4 nfcvd 
 |-  ( A e. _V -> F/_ x C )
5 4 1 csbiegf 
 |-  ( A e. _V -> [_ A / x ]_ B = C )
6 dfsbcq 
 |-  ( [_ A / x ]_ B = C -> ( [. [_ A / x ]_ B / y ]. ph <-> [. C / y ]. ph ) )
7 3 5 6 3syl 
 |-  ( A e. V -> ( [. [_ A / x ]_ B / y ]. ph <-> [. C / y ]. ph ) )
8 2 7 bitrd 
 |-  ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ph ) )