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

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( b = B -> ( b = { x } <-> B = { x } ) )
2	1	exbidv	|- ( b = B -> ( E. x b = { x } <-> E. x B = { x } ) )
3	2	elabg	|- ( B e. { b | E. x b = { x } } -> ( B e. { b | E. x b = { x } } <-> E. x B = { x } ) )
4	3	ibi	|- ( B e. { b | E. x b = { x } } -> E. x B = { x } )