Theorem rexsngf

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012) (Revised by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rexsngf.1	$$⊢Ⅎx\psi$$
	rexsngf.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexsngf	$$⊢A\in V\to \left(\exists 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		rexsns	$$⊢\exists x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
4	1 2	sbciegf	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
5	3 4	bitrid	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}\phi \leftrightarrow \psi \right)$$