Metamath Proof Explorer


Theorem mofal

Description: There exist at most one set such that F. is true. (Contributed by Anthony Hart, 13-Sep-2011)

Ref Expression
Assertion mofal ∃* 𝑥

Proof

Step Hyp Ref Expression
1 nexfal ¬ ∃ 𝑥
2 exmo ( ∃ 𝑥 ⊥ ∨ ∃* 𝑥 ⊥ )
3 1 2 mtpor ∃* 𝑥