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