This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } } )