Theorem eqss 2074

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 1106	. 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 1469	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 2055	. . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
4		dfss2 2055	. . 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 953   = wceq 955   e. wcel 957   (_ wss 2044

This theorem is referenced by:  eqssi 2075  eqssd 2076  ssid 2077  sseq1 2079  sseq2 2080  dfpss3 2131  uneqin 2253  ss0b 2299  vss 2304  pssdifn0 2326  pwpw0 2466  sssn 2470  unidif 2526  ssunieq 2527  intmin 2549  iuneq1 2571  iuneq2 2574  iunxdif2 2594  ssext 2759  pweqb 2761  pwun 2825  poeq2 2839  soeq2 2850  iunpw 2910  freq2 2919  oneqmini 3013  orduniorsuc 3083  tfi 3122  eqrel 3246  cnveq 3288  dmeq 3307  relssres 3388  xp11 3472  ssrnres 3477  funeq 3531  dff2 3812  fconst4 3846  tz7.49 3954  oawordeulem 4181  ixpeq2 4348  sbthlem3 4438  rankc1 4688  carden 4814  iscard 4836  iscard2 4837  aleph11 4862  cardaleph 4868  cflim 4892  iscld4 7656  0ntr 7662  opnneiid 7697  shlesb1 9314  shle0t 9321  orthin 9325  chcon2 9342  chcon3 9344  chlejb1 9354  chabs2t 9395  h1datom 9461  cmbr4 9501  osum 9543  osumcor2 9547  pjjs 9602  pjin2 10077  stcltr2 10158  mdbr2 10179  dmdbr2 10186  mdsl2 10205  mdsl2b 10206  mdslmd3 10215  chrelat4 10256  sumdmdlem2 10302  dmdbr5at 10305  uninqs 10400  oefil2 10500  filintf 10502  rcfpfillem2 10512

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-in 2048  df-ss 2050

Copyright terms: Public domain