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 3143). (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 3140 | . 2 wff ∃!𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1536 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2114 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 398 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2653 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 208 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: reuanid 3328 nfreu1 3370 nfreud 3372 nfreuw 3374 reubida 3387 reubidva 3388 reubiia 3390 reueq1f 3399 reueq1 3407 reu5 3430 rmo5 3434 reueubd 3436 cbvreuw 3443 cbvreu 3447 reuv 3521 reu2 3716 reu6 3717 reu3 3718 2reuswap 3737 2reuswap2 3738 2reu5lem1 3746 cbvreucsf 3927 reuss2 4283 reuun2 4286 reupick 4287 reupick3 4288 euelss 4290 reusn 4663 rabsneu 4665 reusv2lem4 5302 reusv2lem5 5303 reuhypd 5320 funcnv3 6424 feu 6554 dff4 6867 f1ompt 6875 fsn 6897 riotauni 7120 riotacl2 7130 riota1 7135 riota1a 7136 riota2df 7137 snriota 7147 riotaund 7153 aceq1 9543 dfac2b 9556 nqerf 10352 zmin 12345 climreu 14913 divalglem10 15753 divalgb 15755 uptx 22233 txcn 22234 q1peqb 24748 axcontlem2 26751 edgnbusgreu 27149 nbusgredgeu0 27150 frgr3vlem2 28053 3vfriswmgrlem 28056 frgrncvvdeqlem2 28079 adjeu 29666 reuxfrdf 30255 rmoxfrd 30257 neibastop3 33710 cbvreud 34657 poimirlem25 34932 poimirlem27 34934 pairreueq 43692 prprsprreu 43701 prprreueq 43702 |
Copyright terms: Public domain | W3C validator |