Theorem eu5 1407

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 969	. . 3 |- (ph -> A.yph)
2	1	eu3 1395	. 2 |- (E!xph <-> (E.xph /\ E.yA.x(ph -> x = y)))
3	1	mo2 1398	. . 3 |- (E*xph <-> E.yA.x(ph -> x = y))
4	3	anbi2i 480	. 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 952  E.wex 978  E!weu 1378  E*wmo 1379

This theorem is referenced by:  eu4 1408  eumo 1409  exmoeu2 1412  euan 1426  euor2 1435  2euex 1439  2euswap 1443  2exeu 1444  2eu1 1447  reu5 1925  reuss2 2271  funcnv3 3550  dff2 3808  aceq6b 4722  recmulpq 5050

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381

Copyright terms: Public domain