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

Proof

Step	Hyp	Ref	Expression
1		ordelssne	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\in B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)\right)$$
2		df-pss	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)$$
3	1 2	bitr4di	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\in B\leftrightarrow A\subset B\right)$$