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	⊢ ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → ∃ 𝑥 𝐵 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 = { 𝑥 } ↔ 𝐵 = { 𝑥 } ) )
2	1	exbidv	⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑥 𝑏 = { 𝑥 } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
3	2	elabg	⊢ ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
4	3	ibi	⊢ ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → ∃ 𝑥 𝐵 = { 𝑥 } )