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 2647 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 2647 was then proved as dfeu 2674. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2151. (Revised by SN, 21-Sep-2023.) |
Ref | Expression |
---|---|
eu6 | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfmoeu 2611 | . . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
2 | 1 | anbi2i 622 | . . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) |
3 | abai 822 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))) | |
4 | eu3v 2648 | . . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | |
5 | 2, 3, 4 | 3bitr4ri 305 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
6 | abai 822 | . . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑))) | |
7 | ancom 461 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑)) | |
8 | biimpr 221 | . . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑)) | |
9 | 8 | alimi 1803 | . . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
10 | 9 | eximi 1826 | . . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) |
11 | exsbim 1999 | . . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑) |
13 | 12 | biantru 530 | . . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑))) |
14 | 6, 7, 13 | 3bitr4i 304 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
15 | 5, 14 | bitri 276 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 ∃wex 1771 ∃!weu 2646 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-10 2136 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-nf 1776 df-mo 2615 df-eu 2647 |
This theorem is referenced by: euf 2654 nfeu1 2667 dfmo 2675 sb8eulem 2677 reu6 3714 euabsn2 4653 eunex 5281 euotd 5394 iotauni 6323 iota1 6325 iotanul 6326 iotaex 6328 iota4 6329 fv3 6681 eufnfv 6982 seqomlem2 8076 aceq1 9531 dfac5 9542 bnj89 31890 cbveud 34535 wl-eudf 34689 wl-euequf 34691 wl-sb8eut 34694 iotain 40626 iotaexeu 40627 iotasbc 40628 iotavalsb 40642 sbiota1 40643 eusnsn 43138 |
Copyright terms: Public domain | W3C validator |