Theorem rexsns

Description: Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015) (Revised by NM, 22-Aug-2018)

	Ref	Expression
Assertion	rexsns	$$⊢\exists x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
2	1	anbi1i	$$⊢\left(x\in \left\{A\right\}\wedge \phi \right)\leftrightarrow \left(x=A\wedge \phi \right)$$
3	2	exbii	$$⊢\exists x\left(x\in \left\{A\right\}\wedge \phi \right)\leftrightarrow \exists x\left(x=A\wedge \phi \right)$$
4		df-rex	$$⊢\exists x\in \left\{A\right\}\phi \leftrightarrow \exists x\left(x\in \left\{A\right\}\wedge \phi \right)$$
5		sbc5	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \exists x\left(x=A\wedge \phi \right)$$
6	3 4 5	3bitr4i	$$⊢\exists x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$