2eu3 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 2eu3 1494

Description: Double existential uniqueness.

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

**Proof of Theorem 2eu3**
Step	Hyp	Ref	Expression
1		hbmo1 1448	. . . . 5
2	1	19.31 1128	. . . 4 $\/$ $\/$
3	2	albii 1040	. . 3 $\/$ $\/$
4		hbmo1 1448	. . . . 5
5	4	hbal 1046	. . . 4
6	5	19.32 1127	. . 3 $\/$ $\/$
7	3, 6	bitri 180	. 2 $\/$ $\/$
8		2eu1 1492	. . . . . . 7 $/\$
9	8	biimpd 160	. . . . . 6 $/\$
10		ancom 446	. . . . . 6 $/\$ $/\$
11	9, 10	syl6ib 219	. . . . 5 $/\$
12	11	adantld 399	. . . 4 $/\$ $/\$
13		2eu1 1492	. . . . . 6 $/\$
14	13	biimpd 160	. . . . 5 $/\$
15	14	adantrd 400	. . . 4 $/\$ $/\$
16	12, 15	jaoi 348	. . 3 $\/$ $/\$ $/\$
17		2exeu 1489	. . . 4 $/\$
18		2exeu 1489	. . . . 5 $/\$
19	18	ancoms 447	. . . 4 $/\$
20	17, 19	jca 295	. . 3 $/\$ $/\$
21	16, 20	impbid1 528	. 2 $\/$ $/\$ $/\$
22	7, 21	sylbi 206	1 $\/$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3

wb 153 $\/$ wo 229 $/\$ wa 230

wal 995

wex 1021

weu 1422

wmo 1423

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-10 1007 ax-11 1008 ax-12 1009 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260

This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-ex 1022 df-sb 1214 df-eu 1424 df-mo 1425