# Metamath Proof Explorer

## 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}↔\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$

### Proof

Step Hyp Ref Expression
1 albiim ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {A}\right)\right)$
2 dfcleq ${⊢}{A}={B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)$
3 dfss2 ${⊢}{A}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)$
4 dfss2 ${⊢}{B}\subseteq {A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {A}\right)$
5 3 4 anbi12i ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {A}\right)\right)$
6 1 2 5 3bitr4i ${⊢}{A}={B}↔\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$