Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-reu | Structured version Visualization version 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 2914 | . 2 |
5 | 2 | cv 1482 | . . . . 5 |
6 | 5, 3 | wcel 1990 | . . . 4 |
7 | 6, 1 | wa 384 | . . 3 |
8 | 7, 2 | weu 2470 | . 2 |
9 | 4, 8 | wb 196 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: nfreu1 3110 nfreud 3112 reubida 3124 reubiia 3127 reueq1f 3136 reu5 3159 rmo5 3162 reueubd 3164 cbvreu 3169 reuv 3221 reu2 3394 reu6 3395 reu3 3396 2reuswap 3410 2reu5lem1 3413 cbvreucsf 3567 reuss2 3907 reuun2 3910 reupick 3911 reupick3 3912 euelss 3914 reusn 4262 rabsneu 4264 reusv2lem4 4872 reusv2lem5 4873 reuhypd 4895 funcnv3 5959 feu 6080 dff4 6373 f1ompt 6382 fsn 6402 riotauni 6617 riotacl2 6624 riota1 6629 riota1a 6630 riota2df 6631 snriota 6641 riotaund 6647 aceq1 8940 dfac2 8953 nqerf 9752 zmin 11784 climreu 14287 divalglem10 15125 divalgb 15127 uptx 21428 txcn 21429 q1peqb 23914 axcontlem2 25845 edgnbusgreu 26269 nbusgredgeu0 26270 frgr3vlem2 27138 3vfriswmgrlem 27141 frgrncvvdeqlem2 27164 adjeu 28748 2reuswap2 29328 rmoxfrdOLD 29332 rmoxfrd 29333 neibastop3 32357 poimirlem25 33434 poimirlem27 33436 |
Copyright terms: Public domain | W3C validator |