![]() |
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 2535 was then proved as dfmo 2591. (Revised by BJ, 30-Sep-2022.) |
Ref | Expression |
---|---|
moeu | ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | moabs 2538 | . 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) | |
2 | exmoeub 2575 | . . 3 ⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑)) | |
3 | 2 | pm5.74i 271 | . 2 ⊢ ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
4 | 1, 3 | bitri 275 | 1 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∃wex 1782 ∃*wmo 2533 ∃!weu 2563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-mo 2535 df-eu 2564 |
This theorem is referenced by: dfeu 2590 dfmo 2591 sb8mo 2596 cbvmowOLD 2599 2euexv 2628 2euex 2638 2eu1 2647 2eu1v 2648 rmo5 3397 funeu 6574 dffun8 6577 modom 9244 climmo 15501 rmoxfrd 31733 nmotru 35293 bj-moeub 35728 wl-sb8mot 36443 nexmo1 37114 moeu2 37231 moxfr 41430 funressneu 45757 funressndmafv2rn 45931 |
Copyright terms: Public domain | W3C validator |