Theorem ordelpss

Description: For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of TakeutiZaring p. 37. (Contributed by NM, 17-Jun-1998)

	Ref	Expression
Assertion	ordelpss	|- ( ( Ord A /\ Ord B ) -> ( A e. B <-> A C. B ) )

Proof

Step	Hyp	Ref	Expression
1		ordelssne	|- ( ( Ord A /\ Ord B ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) )
2		df-pss	|- ( A C. B <-> ( A C_ B /\ A =/= B ) )
3	1 2	bitr4di	|- ( ( Ord A /\ Ord B ) -> ( A e. B <-> A C. B ) )