Theorem nrexrmo 2828

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

Assertion

Ref	Expression
nrexrmo	⊢ (¬ ∃x ∈ A φ → ∃*x ∈ A φ)

Proof of Theorem nrexrmo

Step	Hyp	Ref	Expression
1		pm2.21 100	. 2 ⊢ (¬ ∃x ∈ A φ → (∃x ∈ A φ → ∃!x ∈ A φ))
2		rmo5 2827	. 2 ⊢ (∃*x ∈ A φ ↔ (∃x ∈ A φ → ∃!x ∈ A φ))
3	1, 2	sylibr 203	1 ⊢ (¬ ∃x ∈ A φ → ∃*x ∈ A φ)

Syntax hints:  ¬ wn 3   → wi 4  ∃wrex 2615  ∃!wreu 2616  ∃*wrmo 2617

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-mo 2209  df-rex 2620  df-reu 2621  df-rmo 2622

This theorem is referenced by: (None)