Theorem onsseli

Description: Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995)

	Ref	Expression
Hypotheses	on.1	|- A e. On
	on.2	|- B e. On
Assertion	onsseli	|- ( A C_ B <-> ( A e. B \/ A = B ) )

Proof

Step	Hyp	Ref	Expression
1		on.1	|- A e. On
2		on.2	|- B e. On
3		onsseleq	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
4	1 2 3	mp2an	|- ( A C_ B <-> ( A e. B \/ A = B ) )