![]() |
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 2534 was then proved as dfmo 2590. (Revised by BJ, 30-Sep-2022.) |
Ref | Expression |
---|---|
moeu | ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | moabs 2537 | . 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) | |
2 | exmoeub 2574 | . . 3 ⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑)) | |
3 | 2 | pm5.74i 270 | . 2 ⊢ ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
4 | 1, 3 | bitri 274 | 1 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∃wex 1781 ∃*wmo 2532 ∃!weu 2562 |
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 1913 ax-6 1971 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-mo 2534 df-eu 2563 |
This theorem is referenced by: dfeu 2589 dfmo 2590 sb8mo 2595 cbvmowOLD 2598 2euexv 2627 2euex 2637 2eu1 2646 2eu1v 2647 rmo5 3396 funeu 6570 dffun8 6573 modom 9240 climmo 15497 rmoxfrd 31720 nmotru 35281 bj-moeub 35716 wl-sb8mot 36431 nexmo1 37102 moeu2 37219 moxfr 41415 funressneu 45743 funressndmafv2rn 45917 |
Copyright terms: Public domain | W3C validator |