Theorem discsntermlem

Description: A singlegon is an element of the class of singlegons. The converse ( basrestermcfolem ) also holds. This is trivial if B is b ( abid ). (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Assertion	discsntermlem	$$⊢\exists xB=\left\{x\right\}\to B\in \left\{b|\exists xb=\left\{x\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
2		eleq1	$$⊢B=\left\{x\right\}\to \left(B\in \mathrm{V}\leftrightarrow \left\{x\right\}\in \mathrm{V}\right)$$
3	1 2	mpbiri	$$⊢B=\left\{x\right\}\to B\in \mathrm{V}$$
4	3	exlimiv	$$⊢\exists xB=\left\{x\right\}\to B\in \mathrm{V}$$
5		eqeq1	$$⊢b=B\to \left(b=\left\{x\right\}\leftrightarrow B=\left\{x\right\}\right)$$
6	5	exbidv	$$⊢b=B\to \left(\exists xb=\left\{x\right\}\leftrightarrow \exists xB=\left\{x\right\}\right)$$
7	6	elabg	$$⊢B\in \mathrm{V}\to \left(B\in \left\{b|\exists xb=\left\{x\right\}\right\}\leftrightarrow \exists xB=\left\{x\right\}\right)$$
8	4 7	syl	$$⊢\exists xB=\left\{x\right\}\to \left(B\in \left\{b|\exists xb=\left\{x\right\}\right\}\leftrightarrow \exists xB=\left\{x\right\}\right)$$
9	8	ibir	$$⊢\exists xB=\left\{x\right\}\to B\in \left\{b|\exists xb=\left\{x\right\}\right\}$$