Theorem 2eu8 2291

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 2290. (Contributed by NM, 20-Feb-2005.)

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 2285	. . 3 |- (E!xE.yph -> (E!yE!xph <-> E!yE.xph))
2	1	pm5.32i 618	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> (E!xE.yph /\ E!yE.xph))
3		nfeu1 2214	. . . . 5 |- F/xE!xph
4	3	nfeu 2220	. . . 4 |- F/xE!yE!xph
5	4	euan 2261	. . 3 |- (E!x(E!yE!xph /\ E.yph) <-> (E!yE!xph /\ E!xE.yph))
6		ancom 437	. . . . . 6 |- ((E!xph /\ E.yph) <-> (E.yph /\ E!xph))
7	6	eubii 2213	. . . . 5 |- (E!y(E!xph /\ E.yph) <-> E!y(E.yph /\ E!xph))
8		nfe1 1732	. . . . . 6 |- F/yE.yph
9	8	euan 2261	. . . . 5 |- (E!y(E.yph /\ E!xph) <-> (E.yph /\ E!yE!xph))
10		ancom 437	. . . . 5 |- ((E.yph /\ E!yE!xph) <-> (E!yE!xph /\ E.yph))
11	7, 9, 10	3bitri 262	. . . 4 |- (E!y(E!xph /\ E.yph) <-> (E!yE!xph /\ E.yph))
12	11	eubii 2213	. . 3 |- (E!xE!y(E!xph /\ E.yph) <-> E!x(E!yE!xph /\ E.yph))
13		ancom 437	. . 3 |- ((E!xE.yph /\ E!yE!xph) <-> (E!yE!xph /\ E!xE.yph))
14	5, 12, 13	3bitr4ri 269	. 2 |- ((E!xE.yph /\ E!yE!xph) <-> E!xE!y(E!xph /\ E.yph))
15		2eu7 2290	. 2 |- ((E!xE.yph /\ E!yE.xph) <-> E!xE!y(E.xph /\ E.yph))
16	2, 14, 15	3bitr3ri 267	1 |- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))

Syntax hints:   <-> wb 176   /\ wa 358  E.wex 1541  E!weu 2204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209

This theorem is referenced by: (None)