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

Theorem eu2 2229
 Description: An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.)
Hypothesis
Ref Expression
eu2.1 yφ
Assertion
Ref Expression
eu2 (∃!xφ ↔ (xφ xy((φ [y / x]φ) → x = y)))
Distinct variable group:   x,y
Allowed substitution hints:   φ(x,y)

Proof of Theorem eu2
StepHypRef Expression
1 euex 2227 . . 3 (∃!xφxφ)
2 eu2.1 . . . . 5 yφ
32eumo0 2228 . . . 4 (∃!xφyx(φx = y))
42mo 2226 . . . 4 (yx(φx = y) ↔ xy((φ [y / x]φ) → x = y))
53, 4sylib 188 . . 3 (∃!xφxy((φ [y / x]φ) → x = y))
61, 5jca 518 . 2 (∃!xφ → (xφ xy((φ [y / x]φ) → x = y)))
7 19.29r 1597 . . . 4 ((xφ xy((φ [y / x]φ) → x = y)) → x(φ y((φ [y / x]φ) → x = y)))
8 impexp 433 . . . . . . . . 9 (((φ [y / x]φ) → x = y) ↔ (φ → ([y / x]φx = y)))
98albii 1566 . . . . . . . 8 (y((φ [y / x]φ) → x = y) ↔ y(φ → ([y / x]φx = y)))
10219.21 1796 . . . . . . . 8 (y(φ → ([y / x]φx = y)) ↔ (φy([y / x]φx = y)))
119, 10bitri 240 . . . . . . 7 (y((φ [y / x]φ) → x = y) ↔ (φy([y / x]φx = y)))
1211anbi2i 675 . . . . . 6 ((φ y((φ [y / x]φ) → x = y)) ↔ (φ (φy([y / x]φx = y))))
13 abai 770 . . . . . 6 ((φ y([y / x]φx = y)) ↔ (φ (φy([y / x]φx = y))))
1412, 13bitr4i 243 . . . . 5 ((φ y((φ [y / x]φ) → x = y)) ↔ (φ y([y / x]φx = y)))
1514exbii 1582 . . . 4 (x(φ y((φ [y / x]φ) → x = y)) ↔ x(φ y([y / x]φx = y)))
167, 15sylib 188 . . 3 ((xφ xy((φ [y / x]φ) → x = y)) → x(φ y([y / x]φx = y)))
172eu1 2225 . . 3 (∃!xφx(φ y([y / x]φx = y)))
1816, 17sylibr 203 . 2 ((xφ xy((φ [y / x]φ) → x = y)) → ∃!xφ)
196, 18impbii 180 1 (∃!xφ ↔ (xφ xy((φ [y / x]φ) → x = y)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544  [wsb 1648  ∃!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 This theorem is referenced by:  eu3  2230  bm1.1  2338  reu2  3024
 Copyright terms: Public domain W3C validator