2eu5 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 2eu5 1446

Description: An alternate definition of double existential uniqueness (see 2eu4 1445). 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.")

**Assertion**
Ref	Expression
2eu5	$/\$ $/\$ $/\$

Distinct variable groups:

**Proof of Theorem 2eu5**
Step	Hyp	Ref	Expression
1		2eu1 1442	. . 3 $/\$
2	1	pm5.32ri 644	. 2 $/\$ $/\$ $/\$
3		eumo 1404	. . . . 5
4	3	adantl 388	. . . 4 $/\$
5		2moex 1433	. . . 4
6	4, 5	syl 10	. . 3 $/\$
7	6	pm4.71i 635	. 2 $/\$ $/\$ $/\$
8		2eu4 1445	. 2 $/\$ $/\$ $/\$
9	2, 7, 8	3bitr2 179	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3

wb 146 $/\$ wa 223

wal 951

wceq 953

wex 977

weu 1373

wmo 1374

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376