HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eqss 2067
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
StepHypRef Expression
1 albi 1103 . 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 1463 . 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3 dfss2 2048 . . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
4 dfss2 2048 . . 3 |- (B (_ A <-> A.x(x e. B -> x e. A))
53, 4anbi12i 481 . 2 |- ((A (_ B /\ B (_ A) <-> (A.x(x e. A -> x e. B) /\ A.x(x e. B -> x e. A)))
61, 2, 53bitr4 183 1 |- (A = B <-> (A (_ B /\ B (_ A))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955   (_ wss 2037
This theorem is referenced by:  eqssi 2068  eqssd 2069  ssid 2070  sseq1 2072  sseq2 2073  dfpss3 2124  uneqin 2246  ss0b 2292  vss 2297  pssdifn0 2319  pwpw0 2460  sssn 2464  unidif 2520  ssunieq 2521  intmin 2543  iuneq1 2565  iuneq2 2568  iunxdif2 2588  ssext 2753  pweqb 2755  pwun 2818  poeq2 2834  soeq2 2845  iunpw 2904  freq2 2913  oneqmini 3007  orduniorsuc 3077  tfi 3116  eqrel 3240  cnveq 3281  dmeq 3300  relssres 3376  xp11 3463  ssrnres 3467  funeq 3521  dff2 3802  fconst4 3836  tz7.49 3944  oawordeulem 4172  ixpeq2 4339  sbthlem3 4429  rankc1 4677  carden 4803  iscard 4825  iscard2 4826  aleph11 4851  cardaleph 4857  cflim 4881  iscld4 7638  0ntr 7644  opnneiid 7678  shlesb1 9274  shle0t 9281  orthin 9285  chcon2 9302  chcon3 9304  chlejb1 9314  chabs2t 9355  h1datom 9421  cmbr4 9461  osum 9503  osumcor2 9507  pjjs 9562  pjin2 10031  stcltr2 10112  mdbr2 10133  dmdbr2 10140  mdsl2 10157  mdsl2b 10158  mdslmd3 10167  chrelat4 10208  sumdmdlem2 10253  dmdbr5at 10255  uninqs 10342  oefil2 10441  filintf 10443
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043
Copyright terms: Public domain