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	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sspss	$$⊢A\subseteq B\leftrightarrow \left(A\subset B\vee A=B\right)$$
2		ordelpss	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\in B\leftrightarrow A\subset B\right)$$
3	2	orbi1d	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(\left(A\in B\vee A=B\right)\leftrightarrow \left(A\subset B\vee A=B\right)\right)$$
4	1 3	bitr4id	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$