Theorem iota0ndef 47581

Description: Example for an undefined iota being the empty set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). (Contributed by AV, 24-Aug-2022.)

Assertion

Ref	Expression
iota0ndef	⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅

Distinct variable group:   𝑥,𝑦

Proof of Theorem iota0ndef

Step	Hyp	Ref	Expression
1		nalset 5258	. . . 4 ⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
2	1	intnanr 490	. . 3 ⊢ ¬ (∃𝑥∀𝑦 𝑦 ∈ 𝑥 ∧ ∃*𝑥∀𝑦 𝑦 ∈ 𝑥)
3		df-eu 2590	. . 3 ⊢ (∃!𝑥∀𝑦 𝑦 ∈ 𝑥 ↔ (∃𝑥∀𝑦 𝑦 ∈ 𝑥 ∧ ∃*𝑥∀𝑦 𝑦 ∈ 𝑥))
4	2, 3	mtbir 325	. 2 ⊢ ¬ ∃!𝑥∀𝑦 𝑦 ∈ 𝑥
5		iotanul 6490	. 2 ⊢ (¬ ∃!𝑥∀𝑦 𝑦 ∈ 𝑥 → (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅

Syntax hints:  ¬ wn 3   ∧ wa 398  ∀wal 1552   = wceq 1554  ∃wex 1793  ∃*wmo 2558  ∃!weu 2589  ∅c0 4280  ℩cio 6464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-v 3450  df-dif 3902  df-ss 3916  df-nul 4281  df-sn 4577  df-uni 4860  df-iota 6466

This theorem is referenced by: (None)