Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-reu | Unicode version |
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
df-reu |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | cA | . . 3 | |
4 | 1, 2, 3 | wreu 2395 | . 2 |
5 | 2 | cv 1315 | . . . . 5 |
6 | 5, 3 | wcel 1465 | . . . 4 |
7 | 6, 1 | wa 103 | . . 3 |
8 | 7, 2 | weu 1977 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfreu1 2579 nfreudxy 2581 reubida 2589 reubiia 2592 reueq1f 2601 reu5 2620 rmo5 2623 cbvreu 2629 reuv 2679 reu2 2845 reu6 2846 reu3 2847 2reuswapdc 2861 cbvreucsf 3034 reuss2 3326 reuun2 3329 reupick 3330 reupick3 3331 reusn 3564 rabsneu 3566 reuhypd 4362 funcnv3 5155 feu 5275 dff4im 5534 f1ompt 5539 fsn 5560 riotauni 5704 riotacl2 5711 riota1 5716 riota1a 5717 riota2df 5718 snriota 5727 riotaund 5732 acexmid 5741 climreu 11021 divalgb 11534 uptx 12354 txcn 12355 dedekindicc 12691 bdcriota 12977 |
Copyright terms: Public domain | W3C validator |