Theorem sbcnestg

Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcnestgw when possible. (Contributed by NM, 27-Nov-2005) (Proof shortened by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	sbcnestg	|- ( 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		sbcnestgf	|- ( ( 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 ) )