Theorem eu6 2573

Description: Alternate definition of the unique existential quantifier df-eu 2568 not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2568 was then proved as dfeu 2594. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2160. (Revised by SN, 21-Sep-2023.)

Assertion

Ref	Expression
eu6	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eu6

Step	Hyp	Ref	Expression
1		dfmoeu 2535	. . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
2	1	anbi2i 626	. . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
3		abai 827	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
4		eu3v 2569	. . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
5	2, 3, 4	3bitr4ri 307	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
6		abai 827	. . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
7		ancom 464	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8		biimpr 223	. . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
9	8	alimi 1819	. . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
10	9	eximi 1842	. . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
11		exsbim 2011	. . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
12	10, 11	syl 17	. . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
13	12	biantru 533	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
14	6, 7, 13	3bitr4i 306	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
15	5, 14	bitri 278	1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  ∃wex 1787  ∃!weu 2567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-10 2143  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-nf 1792  df-mo 2539  df-eu 2568

This theorem is referenced by:  euf  2575  nfeu1  2587  dfmo  2595  sb8eulem  2597  reu6  3628  euabsn2  4627  eunex  5268  euotd  5381  iotauni  6333  iota1  6335  iotanul  6336  iotaex  6338  iota4  6339  fv3  6713  eufnfv  7023  seqomlem2  8165  aceq1  9696  dfac5  9707  bnj89  32366  cbveud  35229  wl-eudf  35413  wl-euequf  35415  wl-sb8eut  35418  iotain  41649  iotaexeu  41650  iotasbc  41651  iotavalsb  41665  sbiota1  41666  eusnsn  44135  mo0sn  45777