Metamath Proof Explorer


Theorem nexmo1

Description: If there is no case where wff is true, it is true for at most one case. (Contributed by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion nexmo1 ¬ x φ * x φ

Proof

Step Hyp Ref Expression
1 pm2.21 ¬ x φ x φ ∃! x φ
2 moeu * x φ x φ ∃! x φ
3 1 2 sylibr ¬ x φ * x φ