Metamath Proof Explorer

Theorem iota0def

Description: Example for a defined iota being the empty set, i.e., A. y x C_ y is a wff satisfied by a unique value x , namely x = (/) (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022)

		Ref	Expression
	Assertion	iota0def	$⊢ (ι x \| \forall y x \subseteq y) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		al0ssb	$⊢ \forall y x \subseteq y \leftrightarrow x = \emptyset$
3	2	a1i	$⊢ (\emptyset \in V \land \emptyset \in V) \to (\forall y x \subseteq y \leftrightarrow x = \emptyset)$
4	3	iota5	$⊢ (\emptyset \in V \land \emptyset \in V) \to (ι x \| \forall y x \subseteq y) = \emptyset$
5	1 1 4	mp2an	$⊢ (ι x \| \forall y x \subseteq y) = \emptyset$