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 \{A\} φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ$

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

Metamath Proof Explorer