| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-rmo | Structured version Visualization version GIF version | ||
| Description: Define restricted
"at most one". Note: This notation is most often used
to express that 𝜑 holds for at most one element of a
given class
𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example,
asserted when 𝑥 and 𝐴 are disjoint.
Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3062). (Contributed by NM, 16-Jun-2017.) |
| Ref | Expression |
|---|---|
| df-rmo | ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph | . . 3 wff 𝜑 | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | cA | . . 3 class 𝐴 | |
| 4 | 1, 2, 3 | wrmo 3379 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
| 5 | 2 | cv 1539 | . . . . 5 class 𝑥 |
| 6 | 5, 3 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐴 |
| 7 | 6, 1 | wa 395 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
| 8 | 7, 2 | wmo 2538 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
| 9 | 4, 8 | wb 206 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: reu5 3382 mormo 3385 rmobiia 3386 rmoanidOLD 3392 rmobidva 3395 rmo5 3400 cbvrmovw 3403 rmobida 3406 cbvrmow 3409 nfrmo1 3411 nfrmow 3413 rmoeq1 3416 rmoeq1OLD 3418 rmoeq1f 3424 nfrmowOLD 3427 nfrmod 3432 nfrmo 3434 rmov 3511 rmo4 3736 rmo3f 3740 rmoeq 3744 rmoan 3745 rmoim 3746 rmoimi2 3749 2reuswap 3752 2reu5lem2 3762 2rmoswap 3767 rmo2 3887 rmo3 3889 rmob 3890 rmob2 3892 rmoanim 3894 ssrmof 4051 dfdisj2 5112 rmorabex 5465 dffun9 6595 fncnv 6639 iunmapdisj 10063 brdom4 10570 enqeq 10974 2ndcdisj 23464 2ndcdisj2 23465 pjhtheu 31413 pjpreeq 31417 cnlnadjeui 32096 reuxfrdf 32510 rmoxfrd 32512 rmoun 32513 rmounid 32514 cbvdisjf 32584 funcnvmpt 32677 rmoeqi 36188 rmoeqbii 36189 rmoeqbidv 36214 disjeq12dv 36216 cbvrmovw2 36229 cbvrmodavw 36253 cbvrmodavw2 36284 nrmo 36411 alrmomorn 38359 alrmomodm 38360 dfeldisj4 38721 disjres 38745 cdleme0moN 40227 onsucf1olem 43283 tfsconcatlem 43349 modelaxreplem2 44996 rmotru 48723 |
| Copyright terms: Public domain | W3C validator |