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 
|- E* x F.

Proof

Step Hyp Ref Expression
1 nexfal 
 |-  -. E. x F.
2 exmo 
 |-  ( E. x F. \/ E* x F. )
3 1 2 mtpor 
 |-  E* x F.