Theorem eu5 1944

Description: Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)

Assertion

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

Proof of Theorem eu5

Step	Hyp	Ref	Expression
1		euex 1927	. . 3 |- (E!xph -> E.xph)
2		eumo 1929	. . 3 |- (E!xph -> E*xph)
3	1, 2	jca 290	. 2 |- (E!xph -> (E.xph /\ E*xph))
4		df-mo 1901	. . . . 5 |- (E*xph <-> (E.xph -> E!xph))
5	4	biimpi 113	. . . 4 |- (E*xph -> (E.xph -> E!xph))
6	5	imp 115	. . 3 |- ((E*xph /\ E.xph) -> E!xph)
7	6	ancoms 255	. 2 |- ((E.xph /\ E*xph) -> E!xph)
8	3, 7	impbii 117	1 |- (E!xph <-> (E.xph /\ E*xph))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  E.wex 1378  E!weu 1897  E*wmo 1898

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901

This theorem is referenced by:  exmoeu2  1945  euan  1953  eu4  1959  euim  1965  euexex  1982  2euex  1984  2euswapdc  1988  2exeu  1989  reu5  2516  reuss2  3211  funcnv3  4904  fnres  4958  fnopabg  4965  brprcneu  5114  dff3im  5255  recmulnqg  6375