Metamath Proof Explorer

Theorem fzo0

Description: Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzo0 
|- ( A ..^ A ) = (/)

Proof

Step Hyp Ref Expression
1 fzonel 
 |-  -. A e. ( A ..^ A )
2 fzon0 
 |-  ( ( A ..^ A ) =/= (/) <-> A e. ( A ..^ A ) )
3 2 necon1bbii 
 |-  ( -. A e. ( A ..^ A ) <-> ( A ..^ A ) = (/) )
4 1 3 mpbi 
 |-  ( A ..^ A ) = (/)