Theorem sbcgf

Description: Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 11-Oct-2004) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Hypothesis	sbcgf.1	$$⊢Ⅎx\phi$$
Assertion	sbcgf	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcgf.1	$$⊢Ⅎx\phi$$
2		sbctt	$$⊢\left(A\in V\wedge Ⅎx\phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
3	1 2	mpan2	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$