Theorem onelpss

Description: Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995)

	Ref	Expression
Assertion	onelpss	|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( A e. On -> Ord A )
2		eloni	|- ( B e. On -> Ord B )
3		ordelssne	|- ( ( Ord A /\ Ord B ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) )
4	1 2 3	syl2an	|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) )