Theorem fzon0

Description: A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	fzon0	|- ( ( M ..^ N ) =/= (/) <-> M e. ( M ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( ( M ..^ N ) =/= (/) <-> E. x x e. ( M ..^ N ) )
2		elfzolt3b	|- ( x e. ( M ..^ N ) -> M e. ( M ..^ N ) )
3	2	exlimiv	|- ( E. x x e. ( M ..^ N ) -> M e. ( M ..^ N ) )
4	1 3	sylbi	|- ( ( M ..^ N ) =/= (/) -> M e. ( M ..^ N ) )
5		ne0i	|- ( M e. ( M ..^ N ) -> ( M ..^ N ) =/= (/) )
6	4 5	impbii	|- ( ( M ..^ N ) =/= (/) <-> M e. ( M ..^ N ) )