Theorem sbcg

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf . (Contributed by Alan Sare, 10-Nov-2012)

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

Proof

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