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

Theorem eqss 3306
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-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 1618 . 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 2381 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3280 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3280 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 679 . 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 269 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546    = wceq 1649    e. wcel 1717    C_ wss 3263
This theorem is referenced by:  eqssi  3307  eqssd  3308  sseq1  3312  sseq2  3313  eqimss  3343  ssrabeq  3372  dfpss3  3376  uneqin  3535  ss0b  3600  vss  3607  pssdifn0  3632  pwpw0  3889  sssn  3900  ssunsn  3902  pwsnALT  3952  unidif  3989  ssunieq  3990  uniintsn  4029  iuneq1  4048  iuneq2  4051  iunxdif2  4080  ssext  4359  pweqb  4361  eqopab2b  4425  pwun  4432  soeq2  4464  ordtri4  4559  oneqmini  4573  iunpw  4699  orduniorsuc  4750  tfi  4773  eqrel  4905  eqrelrel  4917  coeq1  4970  coeq2  4971  cnveq  4986  dmeq  5010  relssres  5123  xp11  5244  ssrnres  5249  fnres  5501  eqfnfv3  5768  fneqeql2  5778  dff3  5821  fconst4  5895  f1imaeq  5950  eqoprab2b  6071  fo1stres  6309  fo2ndres  6310  tz7.49  6638  oawordeulem  6733  nnacan  6807  nnmcan  6813  ixpeq2  7012  sbthlem3  7155  isinf  7258  ordunifi  7293  inficl  7365  rankr1c  7680  rankc1  7729  iscard  7795  iscard2  7796  carden2  7807  aleph11  7898  cardaleph  7903  alephinit  7909  dfac12a  7961  cflm  8063  cfslb2n  8081  dfacfin7  8212  wrdeq  11665  isumltss  12555  rpnnen2  12752  isprm2  13014  mrcidb2  13770  iscyggen2  15418  iscyg3  15423  lssle0  15953  islpir2  16249  iscss2  16836  ishil2  16869  bastop1  16981  epttop  16996  iscld4  17052  0ntr  17058  opnneiid  17113  isperf2  17138  cnntr  17261  ist1-3  17335  perfcls  17351  cmpfi  17393  iscon2  17398  dfcon2  17403  snfil  17817  filcon  17836  ufileu  17872  alexsubALTlem4  18002  metequiv  18429  shlesb1i  22736  shle0  22792  orthin  22796  chcon2i  22814  chcon3i  22816  chlejb1i  22826  chabs2  22867  h1datomi  22931  cmbr4i  22951  osumcor2i  22994  pjjsi  23050  pjin2i  23544  stcltr2i  23626  mdbr2  23647  dmdbr2  23654  mdsl2i  23673  mdsl2bi  23674  mdslmd3i  23683  chrelat4i  23724  sumdmdlem2  23770  dmdbr5ati  23773  dfon2lem9  25171  wfrlem8  25287  idsset  25454  fneval  26058  equivtotbnd  26178  heiborlem10  26220  isnacs2  26451  mrefg3  26453  pmap11  29876  dia11N  31163  dia2dimlem5  31183  dib11N  31275  dih11  31380  dihglblem6  31455  doch11  31488  mapd11  31754  mapdcnv11N  31774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator