Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > 2eu5  Unicode version 
Description: An alternate definition of double existential uniqueness (see 2eu4 2341). A mistake sometimes made in the literature is to use to mean "exactly one and exactly one ." (For example, see Proposition 7.53 of [TakeutiZaring] p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining as an additional condition. The correct definition apparently has never been published. ( means "exists at most one.") (Contributed by NM, 26Oct2003.) 
Ref  Expression 

2eu5 
Step  Hyp  Ref  Expression 

1  2eu1 2338  . . 3  
2  1  pm5.32ri 620  . 2 
3  eumo 2298  . . . . 5  
4  3  adantl 453  . . . 4 
5  2moex 2329  . . . 4  
6  4, 5  syl 16  . . 3 
7  6  pm4.71i 614  . 2 
8  2eu4 2341  . 2  
9  2, 7, 8  3bitr2i 265  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 177 wa 359 wal 1546 wex 1547 weu 2258 wmo 2259 
This theorem is referenced by: 2reu5lem3 3105 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1552 ax5 1563 ax17 1623 ax9 1662 ax8 1683 ax6 1740 ax7 1745 ax11 1757 ax12 1946 
This theorem depends on definitions: dfbi 178 dfor 360 dfan 361 dftru 1325 dfex 1548 dfnf 1551 dfsb 1656 dfeu 2262 dfmo 2263 
Copyright terms: Public domain  W3C validator 