![]() |
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 3379 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
2 | 1 | simprbi 498 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wrex 3071 ∃!wreu 3375 ∃*wrmo 3376 |
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 206 df-an 398 df-eu 2564 df-rex 3072 df-rmo 3377 df-reu 3378 |
This theorem is referenced by: reuimrmo 3739 reuxfr1d 3744 2reurmo 3753 2rexreu 3756 2reu2 3890 enqeq 10924 eqsqrtd 15309 efgred2 19613 0frgp 19639 frgpnabllem2 19733 frgpcyg 21112 lmieu 28014 poimirlem25 36450 poimirlem26 36451 addinvcom 41247 tfsconcatlem 42018 |
Copyright terms: Public domain | W3C validator |