mosssn2

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024)

		Ref	Expression
	Assertion	mosssn2	$⊢ \exists^{*} x x \in A \leftrightarrow \exists y A \subseteq \{y\}$

Step	Hyp	Ref	Expression
1		19.45v	$⊢ \exists y (A = \emptyset \lor A = \{y\}) \leftrightarrow (A = \emptyset \lor \exists y A = \{y\})$
2		sssn	$⊢ A \subseteq \{y\} \leftrightarrow (A = \emptyset \lor A = \{y\})$
3	2	exbii	$⊢ \exists y A \subseteq \{y\} \leftrightarrow \exists y (A = \emptyset \lor A = \{y\})$
4		mo0sn	$⊢ \exists^{*} x x \in A \leftrightarrow (A = \emptyset \lor \exists y A = \{y\})$
5	1 3 4	3bitr4ri	$⊢ \exists^{*} x x \in A \leftrightarrow \exists y A \subseteq \{y\}$

Metamath Proof Explorer