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 2451 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1347 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2141 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 2020 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2642 rmobida 2656 rmobiia 2659 rmoeq1f 2664 mormo 2681 reu5 2682 rmo5 2685 rmov 2750 rmo4 2923 rmo3f 2927 rmoan 2930 rmoim 2931 rmoimi2 2933 2reuswapdc 2934 2rmorex 2936 rmo2ilem 3044 rmo3 3046 rmob 3047 ssrmof 3210 dfdisj2 3966 dffun9 5225 fncnv 5262 |
Copyright terms: Public domain | W3C validator |