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 1527 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2649 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 207 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: reuanid 3328 nfreu1 3371 nfreud 3373 nfreuw 3375 reubida 3388 reubidva 3389 reubiia 3391 reueq1f 3400 reueq1 3408 reu5 3431 rmo5 3435 reueubd 3437 cbvreuw 3444 cbvreu 3448 reuv 3522 reu2 3715 reu6 3716 reu3 3717 2reuswap 3736 2reuswap2 3737 2reu5lem1 3745 cbvreucsf 3926 reuss2 4282 reuun2 4285 reupick 4286 reupick3 4287 euelss 4289 reusn 4657 rabsneu 4659 reusv2lem4 5293 reusv2lem5 5294 reuhypd 5311 funcnv3 6418 feu 6548 dff4 6860 f1ompt 6868 fsn 6890 riotauni 7109 riotacl2 7119 riota1 7124 riota1a 7125 riota2df 7126 snriota 7136 riotaund 7142 aceq1 9532 dfac2b 9545 nqerf 10341 zmin 12333 climreu 14903 divalglem10 15743 divalgb 15745 uptx 22163 txcn 22164 q1peqb 24677 axcontlem2 26679 edgnbusgreu 27077 nbusgredgeu0 27078 frgr3vlem2 27981 3vfriswmgrlem 27984 frgrncvvdeqlem2 28007 adjeu 29594 reuxfrdf 30183 rmoxfrd 30185 neibastop3 33608 cbvreud 34537 poimirlem25 34799 poimirlem27 34801 pairreueq 43519 prprsprreu 43528 prprreueq 43529 |
Copyright terms: Public domain | W3C validator |