Metamath Proof Explorer


Theorem ordsseleq

Description: For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 sspss
 |-  ( A C_ B <-> ( A C. B \/ A = B ) )
2 ordelpss
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> A C. B ) )
3 2 orbi1d
 |-  ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ A = B ) <-> ( A C. B \/ A = B ) ) )
4 1 3 bitr4id
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )