| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Double existential uniqueness. |
| Ref | Expression |
|---|---|
| 2eu2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eumo 1807 |
. . 3
| |
| 2 | 2moex 1843 |
. . 3
| |
| 3 | 2eu1 1853 |
. . . 4
| |
| 4 | simpl 346 |
. . . 4
| |
| 5 | 3, 4 | syl6bi 231 |
. . 3
|
| 6 | 1, 2, 5 | 3syl 24 |
. 2
|
| 7 | 2exeu 1850 |
. . 3
| |
| 8 | 7 | expcom 403 |
. 2
|
| 9 | 6, 8 | impbid 574 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 2eu8 1860 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 |