Theorem sbc6

Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993) (Proof shortened by Eric Schmidt, 17-Jan-2007)

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

Proof

Step	Hyp	Ref	Expression
1		sbc6.1	$$⊢A\in \mathrm{V}$$
2		sbc6g	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
3	1 2	ax-mp	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)$$