![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-reu | Structured version Visualization version GIF version |
Description: Define restricted
existential uniqueness.
Note: This notation is most often used to express that 𝜑 holds for exactly one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3086). (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
df-reu | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cA | . . 3 class 𝐴 | |
4 | 1, 2, 3 | wreu 3083 | . 2 wff ∃!𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1507 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2051 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 387 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2584 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 198 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: reuanid 3262 nfreu1 3304 nfreud 3306 reubida 3319 reubidva 3320 reubiia 3323 reueq1f 3332 reueq1 3340 reu5 3363 rmo5 3367 reueubd 3369 cbvreu 3374 reuv 3435 reu2 3621 reu6 3622 reu3 3623 2reuswap 3642 2reuswap2 3643 2reu5lem1 3648 cbvreucsf 3815 reuss2 4164 reuun2 4167 reupick 4168 reupick3 4169 euelss 4171 reusn 4533 rabsneu 4535 reusv2lem4 5151 reusv2lem5 5152 reuhypd 5172 funcnv3 6254 feu 6380 dff4 6688 f1ompt 6696 fsn 6718 riotauni 6941 riotacl2 6948 riota1 6953 riota1a 6954 riota2df 6955 snriota 6965 riotaund 6971 aceq1 9335 dfac2b 9348 nqerf 10148 zmin 12156 climreu 14772 divalglem10 15611 divalgb 15613 uptx 21952 txcn 21953 q1peqb 24466 axcontlem2 26469 edgnbusgreu 26867 nbusgredgeu0 26868 frgr3vlem2 27823 3vfriswmgrlem 27826 frgrncvvdeqlem2 27849 adjeu 29462 rmoxfrd 30053 neibastop3 33268 cbvreud 34133 poimirlem25 34395 poimirlem27 34397 pairreueq 43072 prprsprreu 43081 prprreueq 43082 |
Copyright terms: Public domain | W3C validator |