![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eu4 | Structured version Visualization version GIF version |
Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
Ref | Expression |
---|---|
eu4.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
eu4 | ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-eu 2629 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
2 | eu4.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | mo4 2625 | . . 3 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
4 | 3 | anbi2i 625 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
5 | 1, 4 | bitri 278 | 1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1536 ∃wex 1781 ∃*wmo 2596 ∃!weu 2628 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-mo 2598 df-eu 2629 |
This theorem is referenced by: euind 3663 eqeuel 4276 uniintsn 4875 eusv1 5257 omeu 8194 eroveu 8375 climeu 14904 pceu 16173 initoeu2lem2 17267 psgneu 18626 gsumval3eu 19017 frgr3vlem2 28059 3vfriswmgrlem 28062 unirep 35151 rlimdmafv 43733 rlimdmafv2 43814 |
Copyright terms: Public domain | W3C validator |