|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > reurmo | Structured version Visualization version GIF version | ||
| Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) | 
| Ref | Expression | 
|---|---|
| reurmo | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | reu5 3382 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
| 2 | 1 | simprbi 496 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃wrex 3070 ∃!wreu 3378 ∃*wrmo 3379 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-eu 2569 df-rex 3071 df-rmo 3380 df-reu 3381 | 
| This theorem is referenced by: reuimrmo 3751 reuxfr1d 3756 2reurmo 3765 2rexreu 3768 2reu2 3898 enqeq 10974 eqsqrtd 15406 efgred2 19771 0frgp 19797 frgpnabllem2 19892 frgpcyg 21592 lmieu 28792 poimirlem25 37652 poimirlem26 37653 addinvcom 42461 tfsconcatlem 43349 reuxfr1dd 48726 upeu 48928 | 
| Copyright terms: Public domain | W3C validator |