Theorem basrestermcfolem

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

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

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢b=B\to \left(b=\left\{x\right\}\leftrightarrow B=\left\{x\right\}\right)$$
2	1	exbidv	$$⊢b=B\to \left(\exists xb=\left\{x\right\}\leftrightarrow \exists xB=\left\{x\right\}\right)$$
3	2	elabg	$$⊢B\in \left\{b|\exists xb=\left\{x\right\}\right\}\to \left(B\in \left\{b|\exists xb=\left\{x\right\}\right\}\leftrightarrow \exists xB=\left\{x\right\}\right)$$
4	3	ibi	$$⊢B\in \left\{b|\exists xb=\left\{x\right\}\right\}\to \exists xB=\left\{x\right\}$$