HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 2eu2 1854 . . 3 |- (E!xE.yph -> (E!yE!xph <-> E!yE.xph))
21pm5.32i 707 . 2 |- ((E!xE.yph /\ E!yE!xph) <-> (E!xE.yph /\ E!yE.xph))
3 hbeu1 1781 . . . . 5 |- (E!xph -> A.xE!xph)
43hbeu 1782 . . . 4 |- (E!yE!xph -> A.xE!yE!xph)
54euan 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))
76eubii 1780 . . . . 5 |- (E!y(E!xph /\ E.yph) <-> E!y(E.yph /\ E!xph))
8 hbe1 1363 . . . . . 6 |- (E.yph -> A.yE.yph)
98euan 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))
117, 9, 103bitri 194 . . . 4 |- (E!y(E!xph /\ E.yph) <-> (E!yE!xph /\ E.yph))
1211eubii 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))
145, 12, 133bitr4ri 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))
162, 14, 153bitr3ri 199 1 |- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))
Colors of variables: wff set class
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