Theorem eqss 2073

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 1105	. 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 1468	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 2054	. . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
4		dfss2 2054	. . 3 |- (B (_ A <-> A.x(x e. B -> x e. A))
5	3, 4	anbi12i 482	. 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 183	1 |- (A = B <-> (A (_ B /\ B (_ A))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956   (_ wss 2043

This theorem is referenced by:  eqssi 2074  eqssd 2075  ssid 2076  sseq1 2078  sseq2 2079  dfpss3 2130  uneqin 2252  ss0b 2298  vss 2303  pssdifn0 2325  pwpw0 2465  sssn 2469  unidif 2525  ssunieq 2526  intmin 2548  iuneq1 2570  iuneq2 2573  iunxdif2 2593  ssext 2758  pweqb 2760  pwun 2824  poeq2 2838  soeq2 2849  iunpw 2909  freq2 2918  oneqmini 3012  orduniorsuc 3082  tfi 3121  eqrel 3245  cnveq 3287  dmeq 3306  relssres 3384  xp11 3468  ssrnres 3473  funeq 3527  dff2 3808  fconst4 3842  tz7.49 3950  oawordeulem 4178  ixpeq2 4345  sbthlem3 4435  rankc1 4685  carden 4811  iscard 4833  iscard2 4834  aleph11 4859  cardaleph 4865  cflim 4889  iscld4 7646  0ntr 7652  opnneiid 7687  shlesb1 9297  shle0t 9304  orthin 9308  chcon2 9325  chcon3 9327  chlejb1 9337  chabs2t 9378  h1datom 9444  cmbr4 9484  osum 9526  osumcor2 9530  pjjs 9585  pjin2 10059  stcltr2 10140  mdbr2 10161  dmdbr2 10168  mdsl2 10186  mdsl2b 10187  mdslmd3 10196  chrelat4 10237  sumdmdlem2 10282  dmdbr5at 10284  uninqs 10378  oefil2 10477  filintf 10479

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain