Theorem 2eu8 1449

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 1448.

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 1443	. . 3 |- (E!xE.yph -> (E!yE!xph <-> E!yE.xph))
2	1	pm5.32i 643	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> (E!xE.yph /\ E!yE.xph))
3		hbeu1 1381	. . . . 5 |- (E!xph -> A.xE!xph)
4	3	hbeu 1382	. . . 4 |- (E!yE!xph -> A.xE!yE!xph)
5	4	euan 1421	. . 3 |- (E!x(E!yE!xph /\ E.yph) <-> (E!yE!xph /\ E!xE.yph))
6		ancom 435	. . . . . 6 |- ((E!xph /\ E.yph) <-> (E.yph /\ E!xph))
7	6	eubii 1380	. . . . 5 |- (E!y(E!xph /\ E.yph) <-> E!y(E.yph /\ E!xph))
8		hbe1 1012	. . . . . 6 |- (E.yph -> A.yE.yph)
9	8	euan 1421	. . . . 5 |- (E!y(E.yph /\ E!xph) <-> (E.yph /\ E!yE!xph))
10		ancom 435	. . . . 5 |- ((E.yph /\ E!yE!xph) <-> (E!yE!xph /\ E.yph))
11	7, 9, 10	3bitr 177	. . . 4 |- (E!y(E!xph /\ E.yph) <-> (E!yE!xph /\ E.yph))
12	11	eubii 1380	. . 3 |- (E!xE!y(E!xph /\ E.yph) <-> E!x(E!yE!xph /\ E.yph))
13		ancom 435	. . 3 |- ((E!xE.yph /\ E!yE!xph) <-> (E!yE!xph /\ E!xE.yph))
14	5, 12, 13	3bitr4r 184	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> E!xE!y(E!xph /\ E.yph))
15		2eu7 1448	. 2 |- ((E!xE.yph /\ E!yE.xph) <-> E!xE!y(E.xph /\ E.yph))
16	2, 14, 15	3bitr3r 182	1 |- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))

Syntax hints:   <-> wb 146   /\ wa 223  E.wex 977  E!weu 1373

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

Copyright terms: Public domain