![]() |
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 3742 reuxfr1d 3747 2reurmo 3756 2rexreu 3759 2reu2 3893 enqeq 10929 eqsqrtd 15314 efgred2 19621 0frgp 19647 frgpnabllem2 19742 frgpcyg 21129 lmieu 28035 poimirlem25 36513 poimirlem26 36514 addinvcom 41304 tfsconcatlem 42086 |
Copyright terms: Public domain | W3C validator |