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 3143). (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 3141 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1527 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 2616 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 207 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: rmoanid 3329 nfrmo1 3372 nfrmod 3374 nfrmow 3376 nfrmo 3378 rmobida 3393 rmobiia 3396 rmoeq1f 3401 rmoeq1 3409 mormo 3430 reu5 3431 rmo5 3435 rmov 3523 rmo4 3720 rmo3f 3724 rmoeq 3728 rmoan 3729 rmoim 3730 rmoimi2 3733 2reuswap 3736 2reu5lem2 3746 2rmoswap 3751 rmo2 3869 rmo3 3871 rmo3OLD 3872 rmob 3873 rmob2 3875 rmoanim 3877 ssrmof 4031 dfdisj2 5025 rmorabex 5344 dffun9 6378 fncnv 6421 iunmapdisj 9438 brdom4 9941 enqeq 10345 2ndcdisj 21994 2ndcdisj2 21995 pjhtheu 29099 pjpreeq 29103 cnlnadjeui 29782 reuxfrdf 30183 rmoxfrd 30185 rmoun 30186 rmounid 30187 cbvdisjf 30250 funcnvmpt 30341 nrmo 33656 alrmomorn 35495 alrmomodm 35496 dfeldisj4 35835 cdleme0moN 37243 |
Copyright terms: Public domain | W3C validator |