Theorem 2eu8 1499

Description: Two equivalent expressions for double existential uniqueness. Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E!xE!y using 2eu7 1498.

Assertion

Ref	Expression
2eu8	|- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))

Proof of Theorem 2eu8

Step	Hyp	Ref	Expression
1		2eu2 1493	. . 3 |- (E!xE.yph -> (E!yE!xph <-> E!yE.xph))
2	1	pm5.32i 656	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> (E!xE.yph /\ E!yE.xph))
3		hbeu1 1430	. . . . 5 |- (E!xph -> A.xE!xph)
4	3	hbeu 1431	. . . 4 |- (E!yE!xph -> A.xE!yE!xph)
5	4	euan 1470	. . 3 |- (E!x(E!yE!xph /\ E.yph) <-> (E!yE!xph /\ E!xE.yph))
6		ancom 446	. . . . . 6 |- ((E!xph /\ E.yph) <-> (E.yph /\ E!xph))
7	6	eubii 1429	. . . . 5 |- (E!y(E!xph /\ E.yph) <-> E!y(E.yph /\ E!xph))
8		hbe1 1057	. . . . . 6 |- (E.yph -> A.yE.yph)
9	8	euan 1470	. . . . 5 |- (E!y(E.yph /\ E!xph) <-> (E.yph /\ E!yE!xph))
10		ancom 446	. . . . 5 |- ((E.yph /\ E!yE!xph) <-> (E!yE!xph /\ E.yph))
11	7, 9, 10	3bitri 184	. . . 4 |- (E!y(E!xph /\ E.yph) <-> (E!yE!xph /\ E.yph))
12	11	eubii 1429	. . 3 |- (E!xE!y(E!xph /\ E.yph) <-> E!x(E!yE!xph /\ E.yph))
13		ancom 446	. . 3 |- ((E!xE.yph /\ E!yE!xph) <-> (E!yE!xph /\ E!xE.yph))
14	5, 12, 13	3bitr4ri 191	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> E!xE!y(E!xph /\ E.yph))
15		2eu7 1498	. 2 |- ((E!xE.yph /\ E!yE.xph) <-> E!xE!y(E.xph /\ E.yph))
16	2, 14, 15	3bitr3ri 189	1 |- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))

Syntax hints:   <-> wb 153   /\ wa 230  E.wex 1021  E!weu 1422

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

Copyright terms: Public domain