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

Proof

Step	Hyp	Ref	Expression
1		vsnex	⊢ { 𝑥 } ∈ V
2		eleq1	⊢ ( 𝐵 = { 𝑥 } → ( 𝐵 ∈ V ↔ { 𝑥 } ∈ V ) )
3	1 2	mpbiri	⊢ ( 𝐵 = { 𝑥 } → 𝐵 ∈ V )
4	3	exlimiv	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → 𝐵 ∈ V )
5		eqeq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 = { 𝑥 } ↔ 𝐵 = { 𝑥 } ) )
6	5	exbidv	⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑥 𝑏 = { 𝑥 } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
7	6	elabg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
8	4 7	syl	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
9	8	ibir	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } )