![]() |
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. (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 2943 | . 2 wff ∃!𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1522 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2030 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2498 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 196 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfreu1 3139 nfreud 3141 reubida 3154 reubiia 3157 reueq1f 3166 reu5 3189 rmo5 3192 reueubd 3194 cbvreu 3199 reuv 3252 reu2 3427 reu6 3428 reu3 3429 2reuswap 3443 2reu5lem1 3446 cbvreucsf 3600 reuss2 3940 reuun2 3943 reupick 3944 reupick3 3945 euelss 3947 reusn 4294 rabsneu 4296 reusv2lem4 4902 reusv2lem5 4903 reuhypd 4925 funcnv3 5997 feu 6118 dff4 6413 f1ompt 6422 fsn 6442 riotauni 6657 riotacl2 6664 riota1 6669 riota1a 6670 riota2df 6671 snriota 6681 riotaund 6687 aceq1 8978 dfac2 8991 nqerf 9790 zmin 11822 climreu 14331 divalglem10 15172 divalgb 15174 uptx 21476 txcn 21477 q1peqb 23959 axcontlem2 25890 edgnbusgreu 26313 nbusgredgeu0 26314 frgr3vlem2 27254 3vfriswmgrlem 27257 frgrncvvdeqlem2 27280 adjeu 28876 2reuswap2 29455 rmoxfrdOLD 29459 rmoxfrd 29460 neibastop3 32482 poimirlem25 33564 poimirlem27 33566 |
Copyright terms: Public domain | W3C validator |