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 * x

Proof

Step Hyp Ref Expression
1 nexfal ¬ x
2 exmo x * x
3 1 2 mtpor * x