Description: Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023) (Proof shortened by SN, 3-Jul-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eqsnd.1 | ||
eqsnd.2 | |||
Assertion | eqsnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsnd.1 | ||
2 | eqsnd.2 | ||
3 | 1 | ralrimiva | |
4 | 2 | ne0d | |
5 | eqsn | ||
6 | 4 5 | syl | |
7 | 3 6 | mpbird |