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

Theorem 2eu7 2290
 Description: Two equivalent expressions for double existential uniqueness. (Contributed by NM, 19-Feb-2005.)
Assertion
Ref Expression
2eu7 ((∃!xyφ ∃!yxφ) ↔ ∃!x∃!y(xφ yφ))

Proof of Theorem 2eu7
StepHypRef Expression
1 nfe1 1732 . . . 4 xxφ
21nfeu 2220 . . 3 x∃!yxφ
32euan 2261 . 2 (∃!x(∃!yxφ yφ) ↔ (∃!yxφ ∃!xyφ))
4 ancom 437 . . . . 5 ((xφ yφ) ↔ (yφ xφ))
54eubii 2213 . . . 4 (∃!y(xφ yφ) ↔ ∃!y(yφ xφ))
6 nfe1 1732 . . . . 5 yyφ
76euan 2261 . . . 4 (∃!y(yφ xφ) ↔ (yφ ∃!yxφ))
8 ancom 437 . . . 4 ((yφ ∃!yxφ) ↔ (∃!yxφ yφ))
95, 7, 83bitri 262 . . 3 (∃!y(xφ yφ) ↔ (∃!yxφ yφ))
109eubii 2213 . 2 (∃!x∃!y(xφ yφ) ↔ ∃!x(∃!yxφ yφ))
11 ancom 437 . 2 ((∃!xyφ ∃!yxφ) ↔ (∃!yxφ ∃!xyφ))
123, 10, 113bitr4ri 269 1 ((∃!xyφ ∃!yxφ) ↔ ∃!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:  2eu8  2291
 Copyright terms: Public domain W3C validator