![]() |
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 2471 | . 2 wff ∃*𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1363 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2160 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 104 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | wmo 2039 | . 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 105 | 1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2663 rmobida 2677 rmobiia 2680 rmoeq1f 2685 mormo 2702 reu5 2703 rmo5 2706 rmov 2772 rmo4 2945 rmo3f 2949 rmoan 2952 rmoim 2953 rmoimi2 2955 2reuswapdc 2956 2rmorex 2958 rmo2ilem 3067 rmo3 3069 rmob 3070 ssrmof 3233 dfdisj2 3997 dffun9 5264 fncnv 5301 |
Copyright terms: Public domain | W3C validator |