Theorem eqss

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of Suppes p. 22. (Contributed by NM, 21-May-1993)

	Ref	Expression
Assertion	eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )

Proof

Step	Hyp	Ref	Expression
1		albiim	|- ( A. x ( x e. A <-> x e. B ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. B -> x e. A ) ) )
2		dfcleq	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		dfss2	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		dfss2	|- ( B C_ A <-> A. x ( x e. B -> x e. A ) )
5	3 4	anbi12i	|- ( ( A C_ B /\ B C_ A ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. B -> x e. A ) ) )
6	1 2 5	3bitr4i	|- ( A = B <-> ( A C_ B /\ B C_ A ) )