Theorem eqss 2631

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

Assertion

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

Proof of Theorem eqss

Step	Hyp	Ref	Expression
1		albiim 1465	. 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 1878	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 2610	. . 3 |- (A C_ B <-> A.x(x e. A -> x e. B))
4		dfss2 2610	. . 3 |- (B C_ A <-> A.x(x e. B -> x e. A))
5	3, 4	anbi12i 540	. 2 |- ((A C_ B /\ B C_ A) <-> (A.x(x e. A -> x e. B) /\ A.x(x e. B -> x e. A)))
6	1, 2, 5	3bitr4i 200	1 |- (A = B <-> (A C_ B /\ B C_ A))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300   C_ wss 2593

This theorem is referenced by:  eqssi 2632  eqssd 2633  ssidOLD 2635  sseq1 2637  sseq1OLD 2638  sseq2 2639  eqimss 2665  dfpss3 2695  dfpss3OLD 2696  uneqin 2845  uneqinOLD 2846  ss0b 2901  vss 2908  vssOLD 2909  pssdifn0 2936  pwpw0 3134  sssn 3142  pwsnALT 3173  unidif 3210  ssunieq 3211  intminOLD 3238  uniintsn 3253  iuneq1 3269  iuneq2 3273  iunxdif2 3301  ssext 3508  pweqb 3511  pwun 3580  poeq2 3595  soeq2 3609  freq2 3633  ordtri4 3699  oneqmini 3714  iunpw 3858  orduniorsuc 3909  tfi 3937  eqrel 4077  eqrelrel 4085  cnveq 4135  dmeq 4157  relssres 4248  xp11 4347  ssrnres 4354  funeq 4441  eqfnfv3 4769  dff3 4790  fconst4 4827  fo1stres 5036  fo2ndres 5037  tz7.49 5168  oawordeulem 5236  ixpeq2 5414  sbthlem3 5512  ordtypelem7 5690  rankc1 5816  carden 5981  iscard 6005  iscard2 6006  aleph11 6027  cardaleph 6033  cflim 6057  iscld4 8972  0ntr 8978  opnneiid 9013  filintf 10274  oefil2 10275  shlesb1i 10992  shle0 10999  orthin 11003  chcon2i 11020  chcon3i 11022  chlejb1i 11032  chabs2 11073  h1datomi 11137  cmbr4i 11177  osumi 11221  osumcor2i 11225  pjjsi 11280  pjin2i 11766  stcltr2i 11847  mdbr2 11868  dmdbr2 11875  mdsl2i 11894  mdsl2bi 11895  mdslmd3i 11904  chrelat4i 11945  sumdmdlem2 11991  dmdbr5ati 11994  isprm2 13775  dfon2lem9 13857  wfrlem8 13964  idsset 14070  uninqs 14340  domfldrefc 14361  ranfldrefc 14362  domintrefb 14367  twsymr 14394  inposet 14620  dfps2 14634  rcfpfillem2 14929  clindistop 14962  topsinind 14967  ordtypelem7OLD 15381  cnsubsp2 15427  alexsublem4 15440  dfcon2 15442  isufil2 15565  cnpfillim 15589  eqfnfv3OLD 15721  inficl 15757  frfi 15771  totbndss 15937  heiborlem41 15995  pmap11 17242

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain