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 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 ordelssne ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴𝐵 ) ) )
2 df-pss ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴𝐵 ) )
3 1 2 bitr4di ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵𝐴𝐵 ) )