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