Theorem ralsngf

Description: Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by AV, 3-Apr-2023)

	Ref	Expression
Hypotheses	rexsngf.1	$$⊢Ⅎx\psi$$
	rexsngf.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralsngf	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexsngf.1	$$⊢Ⅎx\psi$$
2		rexsngf.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3		ralsnsg	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	1 2	sbciegf	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
5	3 4	bitrd	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \psi \right)$$