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 2654 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 2654 was then proved as dfeu 2681. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2161. (Revised by SN, 21-Sep-2023.) |
Ref | Expression |
---|---|
eu6 | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfmoeu 2618 | . . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
2 | 1 | anbi2i 624 | . . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) |
3 | abai 824 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))) | |
4 | eu3v 2655 | . . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | |
5 | 2, 3, 4 | 3bitr4ri 306 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
6 | abai 824 | . . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑))) | |
7 | ancom 463 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑)) | |
8 | biimpr 222 | . . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑)) | |
9 | 8 | alimi 1812 | . . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
10 | 9 | eximi 1835 | . . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) |
11 | exsbim 2008 | . . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑) |
13 | 12 | biantru 532 | . . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑))) |
14 | 6, 7, 13 | 3bitr4i 305 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
15 | 5, 14 | bitri 277 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1535 ∃wex 1780 ∃!weu 2653 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-nf 1785 df-mo 2622 df-eu 2654 |
This theorem is referenced by: euf 2661 nfeu1 2674 dfmo 2682 sb8eulem 2684 reu6 3717 euabsn2 4661 eunex 5291 euotd 5403 iotauni 6330 iota1 6332 iotanul 6333 iotaex 6335 iota4 6336 fv3 6688 eufnfv 6991 seqomlem2 8087 aceq1 9543 dfac5 9554 bnj89 31991 cbveud 34656 wl-eudf 34823 wl-euequf 34825 wl-sb8eut 34828 iotain 40798 iotaexeu 40799 iotasbc 40800 iotavalsb 40814 sbiota1 40815 eusnsn 43310 |
Copyright terms: Public domain | W3C validator |