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 2418 | . 2 |
5 | 2 | cv 1330 | . . . . 5 |
6 | 5, 3 | wcel 1480 | . . . 4 |
7 | 6, 1 | wa 103 | . . 3 |
8 | 7, 2 | weu 1999 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfreu1 2602 nfreudxy 2604 reubida 2612 reubiia 2615 reueq1f 2624 reu5 2643 rmo5 2646 cbvreu 2652 reuv 2705 reu2 2872 reu6 2873 reu3 2874 2reuswapdc 2888 cbvreucsf 3064 reuss2 3356 reuun2 3359 reupick 3360 reupick3 3361 reusn 3594 rabsneu 3596 reuhypd 4392 funcnv3 5185 feu 5305 dff4im 5566 f1ompt 5571 fsn 5592 riotauni 5736 riotacl2 5743 riota1 5748 riota1a 5749 riota2df 5750 snriota 5759 riotaund 5764 acexmid 5773 climreu 11066 divalgb 11622 uptx 12443 txcn 12444 dedekindicc 12780 bdcriota 13081 |
Copyright terms: Public domain | W3C validator |