2eu3 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 2eu3 1451

Description: Double existential uniqueness.

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

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

Colors of variables: wff set class

Syntax hints:

wi 3

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

wal 954

wex 980

weu 1380

wmo 1381

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-10 966 ax-11 967 ax-12 968 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383