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". (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 2899 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1474 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 2459 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 195 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfrmo1 3090 nfrmod 3092 nfrmo 3094 rmobida 3106 rmobiia 3109 rmoeq1f 3114 mormo 3135 reu5 3136 rmo5 3139 rmov 3195 rmo4 3366 rmoeq 3372 rmoan 3373 rmoim 3374 rmoimi2 3376 2reuswap 3377 2reu5lem2 3381 rmo2 3492 rmo3 3494 rmob 3495 rmob2 3497 dfdisj2 4555 reuxfr2d 4817 rmorabex 4855 dffun9 5832 fncnv 5876 iunmapdisj 8729 brdom4 9233 enqeq 9635 2ndcdisj 21069 2ndcdisj2 21070 pjhtheu 27637 pjpreeq 27641 cnlnadjeui 28320 rmoxfrd 28717 ssrmo 28718 rmo3f 28719 cbvdisjf 28767 funcnvmpt 28851 cdleme0moN 34530 2rmoswap 39833 |
Copyright terms: Public domain | W3C validator |