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 2309 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1242 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1393 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 97 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 1901 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 98 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2482 rmobida 2496 rmobiia 2499 rmoeq1f 2504 mormo 2521 reu5 2522 rmo5 2525 rmov 2574 rmo4 2734 rmoan 2739 rmoim 2740 rmoimi2 2742 2reuswapdc 2743 2rmorex 2745 rmo2ilem 2847 rmo3 2849 rmob 2850 dfdisj2 3747 dffun9 4930 fncnv 4965 |
Copyright terms: Public domain | W3C validator |