![]() |
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 3052). (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 3363 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1533 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2099 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 394 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 2527 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 205 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: reu5 3366 mormo 3369 rmobiia 3370 rmoanidOLD 3376 rmobidva 3379 rmo5 3384 cbvrmovw 3387 rmobida 3390 cbvrmow 3393 nfrmo1 3395 nfrmow 3397 rmoeq1 3401 rmoeq1OLD 3403 rmoeq1f 3407 nfrmowOLD 3410 nfrmod 3415 nfrmo 3417 rmov 3492 rmo4 3724 rmo3f 3728 rmoeq 3732 rmoan 3733 rmoim 3734 rmoimi2 3737 2reuswap 3740 2reu5lem2 3750 2rmoswap 3755 rmo2 3880 rmo3 3882 rmob 3883 rmob2 3885 rmoanim 3887 ssrmof 4047 dfdisj2 5120 rmorabex 5466 dffun9 6588 fncnv 6632 iunmapdisj 10066 brdom4 10573 enqeq 10977 2ndcdisj 23451 2ndcdisj2 23452 pjhtheu 31327 pjpreeq 31331 cnlnadjeui 32010 reuxfrdf 32419 rmoxfrd 32421 rmoun 32422 rmounid 32423 cbvdisjf 32491 funcnvmpt 32584 nrmo 36122 alrmomorn 38056 alrmomodm 38057 dfeldisj4 38418 disjres 38442 cdleme0moN 39924 onsucf1olem 42936 tfsconcatlem 43002 rmotru 48190 |
Copyright terms: Public domain | W3C validator |