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	|- ( E. x B = { x } -> B e. { b | E. x b = { x } } )

Proof

Step	Hyp	Ref	Expression
1		vsnex	|- { x } e. _V
2		eleq1	|- ( B = { x } -> ( B e. _V <-> { x } e. _V ) )
3	1 2	mpbiri	|- ( B = { x } -> B e. _V )
4	3	exlimiv	|- ( E. x B = { x } -> B e. _V )
5		eqeq1	|- ( b = B -> ( b = { x } <-> B = { x } ) )
6	5	exbidv	|- ( b = B -> ( E. x b = { x } <-> E. x B = { x } ) )
7	6	elabg	|- ( B e. _V -> ( B e. { b | E. x b = { x } } <-> E. x B = { x } ) )
8	4 7	syl	|- ( E. x B = { x } -> ( B e. { b | E. x b = { x } } <-> E. x B = { x } ) )
9	8	ibir	|- ( E. x B = { x } -> B e. { b | E. x b = { x } } )