MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqss Structured version   Unicode version

Theorem eqss 3485
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.)
Assertion
Ref Expression
eqss  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )

Proof of Theorem eqss
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 albiim 1746 . 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 2422 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3459 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3459 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 701 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  <->  ( A. x ( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  B  ->  x  e.  A ) ) )
61, 2, 53bitr4i 280 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1870    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  eqssi  3486  eqssd  3487  sseq1  3491  sseq2  3492  eqimss  3522  ssrabeq  3553  dfpss3  3557  uneqin  3730  ss0b  3798  vss  3835  pssdifn0  3861  pwpw0  4151  sssn  4161  ssunsn  4163  pwsnALT  4217  unidif  4255  ssunieq  4256  uniintsn  4296  iuneq1  4316  iuneq2  4319  iunxdif2  4350  ssext  4677  pweqb  4679  eqopab2b  4751  pwun  4762  soeq2  4795  eqrel  4944  eqrelrel  4956  coeq1  5012  coeq2  5013  cnveq  5028  dmeq  5055  relssres  5162  xp11  5292  ssrnres  5295  ordtri4  5479  oneqmini  5493  fnres  5710  eqfnfv3  5993  fneqeql2  6006  dff3  6050  fconst4  6144  f1imaeq  6181  eqoprab2b  6363  iunpw  6619  orduniorsuc  6671  tfi  6694  fo1stres  6831  fo2ndres  6832  wfrlem8  7051  tz7.49  7170  oawordeulem  7263  nnacan  7337  nnmcan  7343  ixpeq2  7544  sbthlem3  7690  isinf  7791  ordunifi  7827  inficl  7945  rankr1c  8291  rankc1  8340  iscard  8408  iscard2  8409  carden2  8420  aleph11  8513  cardaleph  8518  alephinit  8524  dfac12a  8576  cflm  8678  cfslb2n  8696  dfacfin7  8827  wrdeq  12676  isumltss  13884  rpnnen2  14256  isprm2  14603  mrcidb2  15475  iscyggen2  17451  iscyg3  17456  lssle0  18108  islpir2  18410  iscss2  19180  ishil2  19213  bastop1  19940  epttop  19955  iscld4  20012  0ntr  20018  opnneiid  20073  isperf2  20099  cnntr  20222  ist1-3  20296  perfcls  20312  cmpfi  20354  iscon2  20360  dfcon2  20365  snfil  20810  filcon  20829  ufileu  20865  alexsubALTlem4  20996  metequiv  21455  shlesb1i  26874  shle0  26930  orthin  26934  chcon2i  26952  chcon3i  26954  chlejb1i  26964  chabs2  27005  h1datomi  27069  cmbr4i  27089  osumcor2i  27132  pjjsi  27188  pjin2i  27681  stcltr2i  27763  mdbr2  27784  dmdbr2  27791  mdsl2i  27810  mdsl2bi  27811  mdslmd3i  27820  chrelat4i  27861  sumdmdlem2  27907  dmdbr5ati  27910  eqrelrd2  28061  dfon2lem9  30224  idsset  30442  fneval  30793  topdifinfeq  31487  equivtotbnd  31814  heiborlem10  31856  pmap11  33036  dia11N  34325  dia2dimlem5  34345  dib11N  34437  dih11  34542  dihglblem6  34617  doch11  34650  mapd11  34916  mapdcnv11N  34936  isnacs2  35257  mrefg3  35259  prsal  37726
  Copyright terms: Public domain W3C validator