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	⊢ ( ℩ 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		al0ssb	⊢ ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ )
3	2	a1i	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ ) )
4	3	iota5	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ℩ 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅ )
5	1 1 4	mp2an	⊢ ( ℩ 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅