Theorem bnj158

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj158.1	|- D = ( _om \ { (/) } )
Assertion	bnj158	|- ( m e. D -> E. p e. _om m = suc p )

Proof

Step	Hyp	Ref	Expression
1		bnj158.1	|- D = ( _om \ { (/) } )
2	1	eleq2i	|- ( m e. D <-> m e. ( _om \ { (/) } ) )
3		eldifsn	|- ( m e. ( _om \ { (/) } ) <-> ( m e. _om /\ m =/= (/) ) )
4	2 3	bitri	|- ( m e. D <-> ( m e. _om /\ m =/= (/) ) )
5		nnsuc	|- ( ( m e. _om /\ m =/= (/) ) -> E. p e. _om m = suc p )
6	4 5	sylbi	|- ( m e. D -> E. p e. _om m = suc p )