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 B A B

Proof

Step Hyp Ref Expression
1 ordelssne Ord A Ord B A B A B A B
2 df-pss A B A B A B
3 1 2 bitr4di Ord A Ord B A B A B