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

Theorem eu5 2242
 Description: Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
eu5 (∃!xφ ↔ (xφ ∃*xφ))

Proof of Theorem eu5
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 nfv 1619 . . 3 yφ
21eu3 2230 . 2 (∃!xφ ↔ (xφ yx(φx = y)))
31mo2 2233 . . 3 (∃*xφyx(φx = y))
43anbi2i 675 . 2 ((xφ ∃*xφ) ↔ (xφ yx(φx = y)))
52, 4bitr4i 243 1 (∃!xφ ↔ (xφ ∃*xφ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  ∃!weu 2204  ∃*wmo 2205 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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:  eu4  2243  eumo  2244  exmoeu2  2247  euim  2254  euan  2261  2euex  2276  2euswap  2280  2exeu  2281  2eu1  2284  reu5  2824  reuss2  3535  n0moeu  3562  funeu  5131  funcnv3  5157  fnres  5199  fnopabg  5205  dff3  5420  fnce  6176
 Copyright terms: Public domain W3C validator