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 2898 | . 2 wff ∃!𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1474 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2458 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 195 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfreu1 3089 nfreud 3091 reubida 3101 reubiia 3104 reueq1f 3113 reu5 3136 rmo5 3139 cbvreu 3145 reuv 3194 reu2 3361 reu6 3362 reu3 3363 2reuswap 3377 2reu5lem1 3380 cbvreucsf 3533 reuss2 3866 reuun2 3869 reupick 3870 reupick3 3871 euelss 3873 reusn 4206 rabsneu 4208 reusv2lem4 4798 reusv2lem5 4799 reuhypd 4821 funcnv3 5873 feu 5993 dff4 6281 f1ompt 6290 fsn 6308 riotauni 6517 riotacl2 6524 riota1 6529 riota1a 6530 riota2df 6531 snriota 6540 riotaund 6546 aceq1 8823 dfac2 8836 nqerf 9631 zmin 11660 climreu 14135 divalglem10 14963 divalgb 14965 uptx 21238 txcn 21239 q1peqb 23718 axcontlem2 25645 frgra3vlem2 26528 3vfriswmgralem 26531 frgrancvvdeqlem3 26559 frgraeu 26581 adjeu 28132 2reuswap2 28712 rmoxfrdOLD 28716 rmoxfrd 28717 neibastop3 31527 poimirlem25 32604 poimirlem27 32606 edgnbusgreu 40595 nbusgredgeu0 40596 frgr3vlem2 41444 3vfriswmgrlem 41447 frgrncvvdeqlem3 41471 frgreu 41491 |
Copyright terms: Public domain | W3C validator |