Theorem eqss 1516

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22.

Assertion

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

Proof of Theorem eqss

Step	Hyp	Ref	Expression
1		albi 785	. 2 |- (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 1098	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 1497	. . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
4		dfss2 1497	. . 3 |- (B (_ A <-> A.x(x e. B -> x e. A))
5	3, 4	anbi12i 369	. 2 |- ((A (_ B /\ B (_ A) <-> (A.x(x e. A -> x e. B) /\ A.x(x e. B -> x e. A)))
6	1, 2, 5	3bitr4 158	1 |- (A = B <-> (A (_ B /\ B (_ A))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672   = wceq 1091   e. wcel 1092   (_ wss 1487

This theorem is referenced by:  eqssi 1517  eqssd 1518  ssid 1519  sseq1 1521  sseq2 1522  dfpss3 1558  ss0b 1726  vss 1729  pssdifn0 1750  sssn 1852  ssext 1865  pweqb 1867  pw0 1882  pwpw0 1883  pwun 1918  unidif 1943  ssunieq 1945  intmin 1982  iuneq1 2003  iuneq2 2006  iunpw 2040  poeq2 2131  soeq2 2142  freq2 2175  tfi 2244  oneqmini 2272  orduniorsuc 2337  cleqrel 2483  cnveq 2513  dmeq 2531  relssres 2596  funeq 2683  tz7.49 2997  oawordeulem 3156  sbthlem3 3351  carden 3638  iscard 3659  iscard2 3660  aleph11 3684  cardaleph 3690  cflim 3704  shlesb1 5360  shle0t 5367  orthin 5371  chcon2 5386  chcon3 5387  chlejb1 5397  chabs2t 5433  h1datom 5483  cmbr4 5510  osum 5538  pjjs 5585  pjin2 5647  stcltr2 5708  mdbr2 5728  dmdbr2 5733  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org