Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > moeu | Structured version Visualization version GIF version |
Description: Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995.) This used to be the definition of the at-most-one quantifier, while df-mo 2622 was then proved as dfmo 2682. (Revised by BJ, 30-Sep-2022.) |
Ref | Expression |
---|---|
moeu | ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | moabs 2625 | . 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) | |
2 | exmoeub 2665 | . . 3 ⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑)) | |
3 | 2 | pm5.74i 273 | . 2 ⊢ ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
4 | 1, 3 | bitri 277 | 1 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∃wex 1780 ∃*wmo 2620 ∃!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 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-mo 2622 df-eu 2654 |
This theorem is referenced by: dfeu 2681 dfmo 2682 sb8mo 2687 cbvmow 2688 2euexv 2716 2euex 2726 2eu1 2735 2eu1v 2736 rmo5 3434 funeu 6380 dffun8 6383 modom 8719 climmo 14914 rmoxfrd 30257 nmotru 33756 amosym1 33774 bj-moeub 34173 wl-sb8mot 34829 nexmo1 35523 moxfr 39309 funressneu 43302 funressndmafv2rn 43442 |
Copyright terms: Public domain | W3C validator |