Theorem sbcth

Description: A substitution into a theorem remains true (when A is a set). (Contributed by NM, 5-Nov-2005)

	Ref	Expression
Hypothesis	sbcth.1	$$⊢\phi$$
Assertion	sbcth	$$⊢A\in V\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbcth.1	$$⊢\phi$$
2	1	ax-gen	$$⊢\forall x\phi$$
3		spsbc	$$⊢A\in V\to \left(\forall x\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	2 3	mpi	$$⊢A\in V\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$