Theorem sbcth2

Description: A substitution into a theorem. (Contributed by NM, 1-Mar-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypothesis	sbcth2.1	|- ( x e. B -> ph )
Assertion	sbcth2	|- ( A e. B -> [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcth2.1	|- ( x e. B -> ph )
2	1	rgen	|- A. x e. B ph
3		rspsbc	|- ( A e. B -> ( A. x e. B ph -> [. A / x ]. ph ) )
4	2 3	mpi	|- ( A e. B -> [. A / x ]. ph )