2eu3 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 2eu3 1444

Description: Double existential uniqueness.

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

**Proof of Theorem 2eu3**
Step	Hyp	Ref	Expression
1		hbmo1 1399	. . . . 5
2	1	19.31 1083	. . . 4 $\/$ $\/$
3	2	albii 996	. . 3 $\/$ $\/$
4		hbmo1 1399	. . . . 5
5	4	hbal 1002	. . . 4
6	5	19.32 1082	. . 3 $\/$ $\/$
7	3, 6	bitr 173	. 2 $\/$ $\/$
8		2eu1 1442	. . . . . . 7 $/\$
9	8	biimpd 153	. . . . . 6 $/\$
10		ancom 435	. . . . . 6 $/\$ $/\$
11	9, 10	syl6ib 212	. . . . 5 $/\$
12	11	adantld 390	. . . 4 $/\$ $/\$
13		2eu1 1442	. . . . . 6 $/\$
14	13	biimpd 153	. . . . 5 $/\$
15	14	adantrd 391	. . . 4 $/\$ $/\$
16	12, 15	jaoi 341	. . 3 $\/$ $/\$ $/\$
17		2exeu 1439	. . . 4 $/\$
18		2exeu 1439	. . . . 5 $/\$
19	18	ancoms 436	. . . 4 $/\$
20	17, 19	jca 288	. . 3 $/\$ $/\$
21	16, 20	impbid1 515	. 2 $\/$ $/\$ $/\$
22	7, 21	sylbi 199	1 $\/$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3

wb 146 $\/$ wo 222 $/\$ wa 223

wal 951

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