Theorem 2eu8 1860

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

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 1854	. . 3 |- (E!xE.yph -> (E!yE!xph <-> E!yE.xph))
2	1	pm5.32i 707	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> (E!xE.yph /\ E!yE.xph))
3		hbeu1 1781	. . . . 5 |- (E!xph -> A.xE!xph)
4	3	hbeu 1782	. . . 4 |- (E!yE!xph -> A.xE!yE!xph)
5	4	euan 1827	. . 3 |- (E!x(E!yE!xph /\ E.yph) <-> (E!yE!xph /\ E!xE.yph))
6		ancom 482	. . . . . 6 |- ((E!xph /\ E.yph) <-> (E.yph /\ E!xph))
7	6	eubii 1780	. . . . 5 |- (E!y(E!xph /\ E.yph) <-> E!y(E.yph /\ E!xph))
8		hbe1 1363	. . . . . 6 |- (E.yph -> A.yE.yph)
9	8	euan 1827	. . . . 5 |- (E!y(E.yph /\ E!xph) <-> (E.yph /\ E!yE!xph))
10		ancom 482	. . . . 5 |- ((E.yph /\ E!yE!xph) <-> (E!yE!xph /\ E.yph))
11	7, 9, 10	3bitri 194	. . . 4 |- (E!y(E!xph /\ E.yph) <-> (E!yE!xph /\ E.yph))
12	11	eubii 1780	. . 3 |- (E!xE!y(E!xph /\ E.yph) <-> E!x(E!yE!xph /\ E.yph))
13		ancom 482	. . 3 |- ((E!xE.yph /\ E!yE!xph) <-> (E!yE!xph /\ E!xE.yph))
14	5, 12, 13	3bitr4ri 201	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> E!xE!y(E!xph /\ E.yph))
15		2eu7 1859	. 2 |- ((E!xE.yph /\ E!yE.xph) <-> E!xE!y(E.xph /\ E.yph))
16	2, 14, 15	3bitr3ri 199	1 |- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))

Syntax hints:   <-> wb 163   /\ wa 240  E.wex 1326  E!weu 1771

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776

Copyright terms: Public domain