Metamath Proof Explorer

Theorem mosneq

Description: There exists at most one set whose singleton is equal to a given class. See also moeq . (Contributed by BJ, 24-Sep-2022)

Ref Expression
Assertion mosneq ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\right\}={A}$

Proof

Step Hyp Ref Expression
1 eqtr3 ${⊢}\left(\left\{{x}\right\}={A}\wedge \left\{{y}\right\}={A}\right)\to \left\{{x}\right\}=\left\{{y}\right\}$
2 vex ${⊢}{x}\in \mathrm{V}$
3 2 sneqr ${⊢}\left\{{x}\right\}=\left\{{y}\right\}\to {x}={y}$
4 1 3 syl ${⊢}\left(\left\{{x}\right\}={A}\wedge \left\{{y}\right\}={A}\right)\to {x}={y}$
5 4 gen2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{{x}\right\}={A}\wedge \left\{{y}\right\}={A}\right)\to {x}={y}\right)$
6 sneq ${⊢}{x}={y}\to \left\{{x}\right\}=\left\{{y}\right\}$
7 6 eqeq1d ${⊢}{x}={y}\to \left(\left\{{x}\right\}={A}↔\left\{{y}\right\}={A}\right)$
8 7 mo4 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\right\}={A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{{x}\right\}={A}\wedge \left\{{y}\right\}={A}\right)\to {x}={y}\right)$
9 5 8 mpbir ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\right\}={A}$