Theorem exmo 2249

Description: Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)

Assertion

Ref	Expression
exmo	|- (E.xph \/ E*xph)

Proof of Theorem exmo

Step	Hyp	Ref	Expression
1		pm2.21 100	. . 3 |- (-. E.xph -> (E.xph -> E!xph))
2		df-mo 2209	. . 3 |- (E*xph <-> (E.xph -> E!xph))
3	1, 2	sylibr 203	. 2 |- (-. E.xph -> E*xph)
4	3	orri 365	1 |- (E.xph \/ E*xph)

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357  E.wex 1541  E!weu 2204  E*wmo 2205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-mo 2209

This theorem is referenced by:  moexex  2273  mo2icl  3016  mosubopt  4613