Theorem exsnrex

Description: There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018)

	Ref	Expression
Assertion	exsnrex	$$⊢\exists xM=\left\{x\right\}\leftrightarrow \exists x\in MM=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vsnid	$$⊢x\in \left\{x\right\}$$
2		eleq2	$$⊢M=\left\{x\right\}\to \left(x\in M\leftrightarrow x\in \left\{x\right\}\right)$$
3	1 2	mpbiri	$$⊢M=\left\{x\right\}\to x\in M$$
4	3	pm4.71ri	$$⊢M=\left\{x\right\}\leftrightarrow \left(x\in M\wedge M=\left\{x\right\}\right)$$
5	4	exbii	$$⊢\exists xM=\left\{x\right\}\leftrightarrow \exists x\left(x\in M\wedge M=\left\{x\right\}\right)$$
6		df-rex	$$⊢\exists x\in MM=\left\{x\right\}\leftrightarrow \exists x\left(x\in M\wedge M=\left\{x\right\}\right)$$
7	5 6	bitr4i	$$⊢\exists xM=\left\{x\right\}\leftrightarrow \exists x\in MM=\left\{x\right\}$$