Theorem eu5 1805

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 1317	. . 3 |- (ph -> A.yph)
2	1	eu3 1792	. 2 |- (E!xph <-> (E.xph /\ E.yA.x(ph -> x = y)))
3	1	mo2 1795	. . 3 |- (E*xph <-> E.yA.x(ph -> x = y))
4	3	anbi2i 538	. 2 |- ((E.xph /\ E*xph) <-> (E.xph /\ E.yA.x(ph -> x = y)))
5	2, 4	bitr4i 193	1 |- (E!xph <-> (E.xph /\ E*xph))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296  E.wex 1326  E!weu 1771  E*wmo 1772

This theorem is referenced by:  eu4 1806  eumo 1807  exmoeu2 1810  euim 1817  euan 1827  euanOLD 1828  euor2OLD 1840  2euex 1844  2euexOLD 1845  2euswap 1849  2exeu 1850  2eu1 1853  reu5 2441  reuss2 2870  n0moeu 2887  funcnv3 4476  dff3 4790  aceq6b 5904  recmulpq 6222  uptx 10226  bnj599 12560  bnj599OLD 12561  bnj151 13243

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776

Copyright terms: Public domain