Theorem eu5 1448

Description: Uniqueness in terms of "at most one."

Assertion

Ref	Expression
eu5	|- (E!xph <-> (E.xph /\ E*xph))

Proof of Theorem eu5

Step	Hyp	Ref	Expression
1		ax-17 1007	. . 3 |- (ph -> A.yph)
2	1	eu3 1436	. 2 |- (E!xph <-> (E.xph /\ E.yA.x(ph -> x = y)))
3	1	mo2 1439	. . 3 |- (E*xph <-> E.yA.x(ph -> x = y))
4	3	anbi2i 483	. 2 |- ((E.xph /\ E*xph) <-> (E.xph /\ E.yA.x(ph -> x = y)))
5	2, 4	bitr4i 174	1 |- (E!xph <-> (E.xph /\ E*xph))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990  E.wex 1016  E!weu 1419  E*wmo 1420

This theorem is referenced by:  eu4 1449  eumo 1450  exmoeu2 1453  euan 1467  euor2 1477  2euex 1481  2euswap 1485  2exeu 1486  2eu1 1489  reu5 1975  reuss2 2327  funcnv3 3663  dff3 3931  aceq6b 4888  recmulpq 5224  uptx 11978

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422

Copyright terms: Public domain