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.

Step	Hyp	Ref	Expression
1		nfv 1619	. . 3 ⊢ Ⅎyφ
2	1	eu3 2230	. 2 ⊢ (∃!xφ ↔ (∃xφ ∧ ∃y∀x(φ → x = y)))
3	1	mo2 2233	. . 3 ⊢ (∃*xφ ↔ ∃y∀x(φ → x = y))
4	3	anbi2i 675	. 2 ⊢ ((∃xφ ∧ ∃*xφ) ↔ (∃xφ ∧ ∃y∀x(φ → x = y)))
5	2, 4	bitr4i 243	1 ⊢ (∃!xφ ↔ (∃xφ ∧ ∃*xφ))

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-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:  eu4  2243  eumo  2244  exmoeu2  2247  euim  2254  euan  2261  2euex  2276  2euswap  2280  2exeu  2281  2eu1  2284  reu5  2825  reuss2  3536  n0moeu  3563  funeu  5132  funcnv3  5158  fnres  5200  fnopabg  5206  dff3  5421  fnce  6177