Theorem eu5 1442

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 1003	. . 3 |- (ph -> A.yph)
2	1	eu3 1430	. 2 |- (E!xph <-> (E.xph /\ E.yA.x(ph -> x = y)))
3	1	mo2 1433	. . 3 |- (E*xph <-> E.yA.x(ph -> x = y))
4	3	anbi2i 482	. 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 986  E.wex 1012  E!weu 1413  E*wmo 1414

This theorem is referenced by:  eu4 1443  eumo 1444  exmoeu2 1447  euan 1461  euor2 1471  2euex 1475  2euswap 1479  2exeu 1480  2eu1 1483  reu5 1967  reuss2 2319  funcnv3 3633  dff3 3893  aceq6b 4828  recmulpq 5159

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416

Copyright terms: Public domain