![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eu6 | Structured version Visualization version GIF version |
Description: Alternate definition of the unique existential quantifier df-eu 2566 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 2566 was then proved as dfeu 2592. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2154. (Revised by SN, 21-Sep-2023.) |
Ref | Expression |
---|---|
eu6 | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfmoeu 2533 | . . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
2 | 1 | anbi2i 623 | . . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) |
3 | abai 827 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))) | |
4 | eu3v 2567 | . . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | |
5 | 2, 3, 4 | 3bitr4ri 304 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
6 | abai 827 | . . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑))) | |
7 | ancom 460 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑)) | |
8 | biimpr 220 | . . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑)) | |
9 | 8 | alimi 1807 | . . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
10 | 9 | eximi 1831 | . . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) |
11 | exsbim 1998 | . . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑) |
13 | 12 | biantru 529 | . . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑))) |
14 | 6, 7, 13 | 3bitr4i 303 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
15 | 5, 14 | bitri 275 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1534 ∃wex 1775 ∃!weu 2565 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-10 2138 ax-12 2174 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1776 df-nf 1780 df-mo 2537 df-eu 2566 |
This theorem is referenced by: euf 2573 nfeu1 2585 dfmo 2593 sb8eulem 2595 reu6 3734 euabsn2 4729 eunex 5395 euotd 5522 iotauni 6537 iota1 6539 iotanul 6540 iotaexOLD 6542 iota4 6543 fv3 6924 eufnfv 7248 seqomlem2 8489 aceq1 10154 dfac5 10166 bnj89 34713 cbveud 37354 wl-eudf 37552 wl-euequf 37554 wl-sb8eut 37558 wl-sb8eutv 37559 iotain 44412 iotaexeu 44413 iotasbc 44414 iotavalsb 44428 sbiota1 44429 eusnsn 46975 mo0sn 48663 |
Copyright terms: Public domain | W3C validator |