Theorem 2eu8 1433

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

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 1427	. . 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 1365	. . . . 5 |- (E!xph -> A.xE!xph)
4	3	hbeu 1366	. . . 4 |- (E!yE!xph -> A.xE!yE!xph)
5	4	euan 1405	. . 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 1364	. . . . 5 |- (E!y(E!xph /\ E.yph) <-> E!y(E.yph /\ E!xph))
8		hbe1 990	. . . . . 6 |- (E.yph -> A.yE.yph)
9	8	euan 1405	. . . . 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 1364	. . 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 1432	. 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 956  E!weu 1357

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360

Copyright terms: Public domain