Theorem eqssi

Description: Infer equality from two subclass relationships. Compare Theorem 4 of Suppes p. 22. (Contributed by NM, 9-Sep-1993)

	Ref	Expression
Hypotheses	eqssi.1	$$⊢A\subseteq B$$
	eqssi.2	$$⊢B\subseteq A$$
Assertion	eqssi	$$⊢A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqssi.1	$$⊢A\subseteq B$$
2		eqssi.2	$$⊢B\subseteq A$$
3		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
4	1 2 3	mpbir2an	$$⊢A=B$$