Theorem aiota0def

Description: Example for a defined alternate 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). This corresponds to iota0def . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiota0def	⊢ ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		al0ssb	⊢ ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ )
3	2	ax-gen	⊢ ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ )
4		eqeq2	⊢ ( 𝑧 = ∅ → ( 𝑥 = 𝑧 ↔ 𝑥 = ∅ ) )
5	4	bibi2d	⊢ ( 𝑧 = ∅ → ( ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = 𝑧 ) ↔ ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ ) ) )
6	5	albidv	⊢ ( 𝑧 = ∅ → ( ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ ) ) )
7		eqeq2	⊢ ( 𝑧 = ∅ → ( ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = 𝑧 ↔ ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅ ) )
8	6 7	imbi12d	⊢ ( 𝑧 = ∅ → ( ( ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = 𝑧 ) → ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = 𝑧 ) ↔ ( ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ ) → ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅ ) ) )
9		aiotaval	⊢ ( ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = 𝑧 ) → ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = 𝑧 )
10	8 9	vtoclg	⊢ ( ∅ ∈ V → ( ∀ 𝑥 ( ∀ 𝑦 𝑥 ⊆ 𝑦 ↔ 𝑥 = ∅ ) → ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅ ) )
11	1 3 10	mp2	⊢ ( ℩' 𝑥 ∀ 𝑦 𝑥 ⊆ 𝑦 ) = ∅