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 | |- ( ( ph /\ x e. A ) -> x = B ) |
|
eqsnd.2 | |- ( ph -> B e. A ) |
||
Assertion | eqsnd | |- ( ph -> A = { B } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsnd.1 | |- ( ( ph /\ x e. A ) -> x = B ) |
|
2 | eqsnd.2 | |- ( ph -> B e. A ) |
|
3 | 1 | ralrimiva | |- ( ph -> A. x e. A x = B ) |
4 | 2 | ne0d | |- ( ph -> A =/= (/) ) |
5 | eqsn | |- ( A =/= (/) -> ( A = { B } <-> A. x e. A x = B ) ) |
|
6 | 4 5 | syl | |- ( ph -> ( A = { B } <-> A. x e. A x = B ) ) |
7 | 3 6 | mpbird | |- ( ph -> A = { B } ) |