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	⊢ 𝐴 ⊆ 𝐵
	eqssi.2	⊢ 𝐵 ⊆ 𝐴
Assertion	eqssi	⊢ 𝐴 = 𝐵

Proof

Step	Hyp	Ref	Expression
1		eqssi.1	⊢ 𝐴 ⊆ 𝐵
2		eqssi.2	⊢ 𝐵 ⊆ 𝐴
3		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
4	1 2 3	mpbir2an	⊢ 𝐴 = 𝐵