Metamath Proof Explorer


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 ) )