Theorem sbcnestgw

Description: Nest the composition of two substitutions. Version of sbcnestg 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
Assertion	sbcnestgw	|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ x ph
2	1	ax-gen	|- A. y F/ x ph
3		sbcnestgfw	|- ( ( A e. V /\ A. y F/ x ph ) -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
4	2 3	mpan2	|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )