Theorem eu5 1411

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 973	. . 3 |- (ph -> A.yph)
2	1	eu3 1399	. 2 |- (E!xph <-> (E.xph /\ E.yA.x(ph -> x = y)))
3	1	mo2 1402	. . 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	bitr4 176	1 |- (E!xph <-> (E.xph /\ E*xph))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 956  E.wex 982  E!weu 1382  E*wmo 1383

This theorem is referenced by:  eu4 1412  eumo 1413  exmoeu2 1416  euan 1430  euor2 1440  2euex 1444  2euswap 1448  2exeu 1449  2eu1 1452  reu5 1932  reuss2 2278  funcnv3 3564  dff2 3823  aceq6b 4752  recmulpq 5082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385

Copyright terms: Public domain