New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  2eu8 GIF version

Theorem 2eu8 2291
 Description: Two equivalent expressions for double existential uniqueness. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!x∃!y using 2eu7 2290. (Contributed by NM, 20-Feb-2005.)
Assertion
Ref Expression
2eu8 (∃!x∃!y(xφ yφ) ↔ ∃!x∃!y(∃!xφ yφ))

Proof of Theorem 2eu8
StepHypRef Expression
1 2eu2 2285 . . 3 (∃!xyφ → (∃!y∃!xφ∃!yxφ))
21pm5.32i 618 . 2 ((∃!xyφ ∃!y∃!xφ) ↔ (∃!xyφ ∃!yxφ))
3 nfeu1 2214 . . . . 5 x∃!xφ
43nfeu 2220 . . . 4 x∃!y∃!xφ
54euan 2261 . . 3 (∃!x(∃!y∃!xφ yφ) ↔ (∃!y∃!xφ ∃!xyφ))
6 ancom 437 . . . . . 6 ((∃!xφ yφ) ↔ (yφ ∃!xφ))
76eubii 2213 . . . . 5 (∃!y(∃!xφ yφ) ↔ ∃!y(yφ ∃!xφ))
8 nfe1 1732 . . . . . 6 yyφ
98euan 2261 . . . . 5 (∃!y(yφ ∃!xφ) ↔ (yφ ∃!y∃!xφ))
10 ancom 437 . . . . 5 ((yφ ∃!y∃!xφ) ↔ (∃!y∃!xφ yφ))
117, 9, 103bitri 262 . . . 4 (∃!y(∃!xφ yφ) ↔ (∃!y∃!xφ yφ))
1211eubii 2213 . . 3 (∃!x∃!y(∃!xφ yφ) ↔ ∃!x(∃!y∃!xφ yφ))
13 ancom 437 . . 3 ((∃!xyφ ∃!y∃!xφ) ↔ (∃!y∃!xφ ∃!xyφ))
145, 12, 133bitr4ri 269 . 2 ((∃!xyφ ∃!y∃!xφ) ↔ ∃!x∃!y(∃!xφ yφ))
15 2eu7 2290 . 2 ((∃!xyφ ∃!yxφ) ↔ ∃!x∃!y(xφ yφ))
162, 14, 153bitr3ri 267 1 (∃!x∃!y(xφ yφ) ↔ ∃!x∃!y(∃!xφ yφ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541  ∃!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)
 Copyright terms: Public domain W3C validator