Theorem ralsnsg

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall x\in \left\{A\right\}\phi \leftrightarrow \forall x\left(x\in \left\{A\right\}\to \phi \right)$$
2		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
3	2	imbi1i	$$⊢\left(x\in \left\{A\right\}\to \phi \right)\leftrightarrow \left(x=A\to \phi \right)$$
4	3	albii	$$⊢\forall x\left(x\in \left\{A\right\}\to \phi \right)\leftrightarrow \forall x\left(x=A\to \phi \right)$$
5	1 4	bitri	$$⊢\forall x\in \left\{A\right\}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)$$
6		sbc6g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
7	5 6	bitr4id	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$