Description: A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | vsnex | ⊢ { 𝑥 } ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsn2 | ⊢ { 𝑥 } = { 𝑥 , 𝑥 } | |
2 | zfpair2 | ⊢ { 𝑥 , 𝑥 } ∈ V | |
3 | 1 2 | eqeltri | ⊢ { 𝑥 } ∈ V |