![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-rmo | 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 2363 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1289 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1439 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 1950 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2540 rmobida 2554 rmobiia 2557 rmoeq1f 2562 mormo 2579 reu5 2580 rmo5 2583 rmov 2640 rmo4 2809 rmo3f 2813 rmoan 2816 rmoim 2817 rmoimi2 2819 2reuswapdc 2820 2rmorex 2822 rmo2ilem 2929 rmo3 2931 rmob 2932 dfdisj2 3830 dffun9 5057 fncnv 5093 |
Copyright terms: Public domain | W3C validator |