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

Proof

Step Hyp Ref Expression
1 sspss ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴 = 𝐵 ) )
2 ordelpss ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵𝐴𝐵 ) )
3 2 orbi1d ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴𝐵𝐴 = 𝐵 ) ↔ ( 𝐴𝐵𝐴 = 𝐵 ) ) )
4 1 3 bitr4id ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴 = 𝐵 ) ) )