Description: For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of TakeutiZaring p. 37. (Contributed by NM, 25-Nov-1995)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ordelssne | |- ( ( Ord A /\ Ord B ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ordtr | |- ( Ord A -> Tr A ) |
|
| 2 | tz7.7 | |- ( ( Ord B /\ Tr A ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) ) |
|
| 3 | 1 2 | sylan2 | |- ( ( Ord B /\ Ord A ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) ) |
| 4 | 3 | ancoms | |- ( ( Ord A /\ Ord B ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) ) |