Theorem eqss 2128

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 1148	. 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 1516	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 2109	. . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
4		dfss2 2109	. . 3 |- (B (_ A <-> A.x(x e. B -> x e. A))
5	3, 4	anbi12i 493	. 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	3bitr4i 190	1 |- (A = B <-> (A (_ B /\ B (_ A))

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230  A.wal 995   = wceq 997   e. wcel 999   (_ wss 2098

This theorem is referenced by:  eqssi 2129  eqssd 2130  ssid 2131  sseq1 2133  sseq2 2134  dfpss3 2185  uneqin 2307  ss0b 2354  vss 2359  pssdifn0 2381  pwpw0 2523  sssn 2527  pwsnALT 2555  unidif 2584  ssunieq 2585  intmin 2607  iuneq1 2629  iuneq2 2632  iunxdif2 2652  ssext 2819  pweqb 2821  pwun 2885  poeq2 2899  soeq2 2910  iunpw 2971  freq2 2980  oneqmini 3074  orduniorsuc 3144  tfi 3183  eqrel 3307  cnveq 3349  dmeq 3368  relssres 3449  xp11 3533  ssrnres 3538  funeq 3592  dff2 3874  fconst4 3908  tz7.49 4017  oawordeulem 4246  ixpeq2 4416  sbthlem3 4512  rankc1 4767  carden 4894  iscard 4918  iscard2 4919  aleph11 4944  cardaleph 4950  cflim 4974  iscld4 7781  0ntr 7787  opnneiid 7822  shlesb1i 9442  shle0 9449  orthin 9453  chcon2i 9470  chcon3i 9472  chlejb1i 9482  chabs2 9523  h1datomi 9587  cmbr4i 9627  osumi 9669  osumcor2i 9673  pjjsi 9728  pjin2i 10205  stcltr2i 10286  mdbr2 10307  dmdbr2 10314  mdsl2i 10333  mdsl2bi 10334  mdslmd3i 10343  chrelat4i 10384  sumdmdlem2 10430  dmdbr5ati 10433  uninqs 10527  inposet 10578  oefil2 10660  filintf 10662  rcfpfillem2 10672

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-in 2102  df-ss 2104

Copyright terms: Public domain