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) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypothesis sbcco3gw.1 x = A B = C
Assertion sbcco3gw A V [˙A / x]˙ [˙B / y]˙ φ [˙C / y]˙ φ

Proof

Step Hyp Ref Expression
1 sbcco3gw.1 x = A B = C
2 sbcnestgw A V [˙A / x]˙ [˙B / y]˙ φ [˙ A / x B / y]˙ φ
3 elex A V A V
4 nfcvd A V _ x C
5 4 1 csbiegf A V A / x B = C
6 dfsbcq A / x B = C [˙ A / x B / y]˙ φ [˙C / y]˙ φ
7 3 5 6 3syl A V [˙ A / x B / y]˙ φ [˙C / y]˙ φ
8 2 7 bitrd A V [˙A / x]˙ [˙B / y]˙ φ [˙C / y]˙ φ