Theorem nrexrmo 2829

Description: Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)

Assertion

Ref	Expression
nrexrmo	|- (-. E.x e. A ph -> E*x e. A ph)

Proof of Theorem nrexrmo

Step	Hyp	Ref	Expression
1		pm2.21 100	. 2 |- (-. E.x e. A ph -> (E.x e. A ph -> E!x e. A ph))
2		rmo5 2828	. 2 |- (E*x e. A ph <-> (E.x e. A ph -> E!x e. A ph))
3	1, 2	sylibr 203	1 |- (-. E.x e. A ph -> E*x e. A ph)

This proof depends on syntax axioms:  -. wn 3   -> wi 4  E.wrex 2616  E!wreu 2617  E*wrmo 2618

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-mo 2209  df-rex 2621  df-reu 2622  df-rmo 2623

This theorem is used by: (None)