Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 2eu3 1069

Description: Double existential uniqueness.

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

**Proof of Theorem 2eu3**
Step	Hyp	Ref	Expression
1		hbmo1 1032	. . . . 5
2	1	19.31 766	. . . 4 $\/$ $\/$
3	2	bial 695	. . 3 $\/$ $\/$
4		hbmo1 1032	. . . . 5
5	4	hbal 700	. . . 4
6	5	19.32 765	. . 3 $\/$ $\/$
7	3, 6	bitr 151	. 2 $\/$ $\/$
8		2eu1 1067	. . . . . . 7 $/\$
9	8	biimpd 135	. . . . . 6 $/\$
10		ancom 333	. . . . . 6 $/\$ $/\$
11	9, 10	syl6ib 185	. . . . 5 $/\$
12	11	adantld 307	. . . 4 $/\$ $/\$
13		2eu1 1067	. . . . . 6 $/\$
14	13	biimpd 135	. . . . 5 $/\$
15	14	adantrd 308	. . . 4 $/\$ $/\$
16	12, 15	jaoi 275	. . 3 $\/$ $/\$ $/\$
17		2exeu 1066	. . . . 5 $/\$
18		2exeu 1066	. . . . . 6 $/\$
19	18	ancoms 334	. . . . 5 $/\$
20	17, 19	jca 236	. . . 4 $/\$ $/\$
21	20	a1i 7	. . 3 $\/$ $/\$ $/\$
22	16, 21	impbid 397	. 2 $\/$ $/\$ $/\$
23	7, 22	sylbi 174	1 $\/$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 2

wb 127 $\/$ wo 195 $/\$ wa 196

wal 672

wex 678

weu 1007

wmo 1008

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-16 922 ax-17 925

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010