![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eu1 | GIF version |
Description: An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
eu1.1 | ⊢ (𝜑 → ∀𝑦𝜑) |
Ref | Expression |
---|---|
eu1 | ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbs1 1938 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
2 | 1 | euf 2031 | . 2 ⊢ (∃!𝑦[𝑦 / 𝑥]𝜑 ↔ ∃𝑥∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑥)) |
3 | eu1.1 | . . 3 ⊢ (𝜑 → ∀𝑦𝜑) | |
4 | 3 | sb8euh 2049 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) |
5 | equcom 1706 | . . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) | |
6 | 5 | imbi2i 226 | . . . . . 6 ⊢ (([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑥)) |
7 | 6 | albii 1470 | . . . . 5 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑥)) |
8 | 3 | sb6rf 1853 | . . . . 5 ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) |
9 | 7, 8 | anbi12i 460 | . . . 4 ⊢ ((∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑥) ∧ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))) |
10 | ancom 266 | . . . 4 ⊢ ((𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)) ↔ (∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦) ∧ 𝜑)) | |
11 | albiim 1487 | . . . 4 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑥) ↔ (∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑥) ∧ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))) | |
12 | 9, 10, 11 | 3bitr4i 212 | . . 3 ⊢ ((𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑥)) |
13 | 12 | exbii 1605 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)) ↔ ∃𝑥∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑥)) |
14 | 2, 4, 13 | 3bitr4i 212 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1351 ∃wex 1492 [wsb 1762 ∃!weu 2026 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-eu 2029 |
This theorem is referenced by: euex 2056 eu2 2070 |
Copyright terms: Public domain | W3C validator |