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

Theorem eqss 3519
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 1675 . 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 2460 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3493 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3493 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 697 . 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 277 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1377    = wceq 1379    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  eqssi  3520  eqssd  3521  sseq1  3525  sseq2  3526  eqimss  3556  ssrabeq  3586  dfpss3  3590  uneqin  3749  ss0b  3815  vss  3863  pssdifn0  3888  pwpw0  4175  sssn  4185  ssunsn  4187  pwsnALT  4240  unidif  4279  ssunieq  4280  uniintsn  4319  iuneq1  4339  iuneq2  4342  iunxdif2  4373  ssext  4702  pweqb  4704  eqopab2b  4777  pwun  4788  soeq2  4820  ordtri4  4915  oneqmini  4929  eqrel  5090  eqrelrel  5102  coeq1  5158  coeq2  5159  cnveq  5174  dmeq  5201  relssres  5309  xp11  5440  ssrnres  5443  fnres  5695  eqfnfv3  5975  fneqeql2  5988  dff3  6032  fconst4  6123  f1imaeq  6159  eqoprab2b  6337  iunpw  6592  orduniorsuc  6643  tfi  6666  fo1stres  6805  fo2ndres  6806  tz7.49  7107  oawordeulem  7200  nnacan  7274  nnmcan  7280  ixpeq2  7480  sbthlem3  7626  isinf  7730  ordunifi  7766  inficl  7881  rankr1c  8235  rankc1  8284  iscard  8352  iscard2  8353  carden2  8364  aleph11  8461  cardaleph  8466  alephinit  8472  dfac12a  8524  cflm  8626  cfslb2n  8644  dfacfin7  8775  wrdeq  12526  isumltss  13619  rpnnen2  13816  isprm2  14080  mrcidb2  14869  iscyggen2  16675  iscyg3  16680  lssle0  17379  islpir2  17681  iscss2  18484  ishil2  18517  bastop1  19261  epttop  19276  iscld4  19332  0ntr  19338  opnneiid  19393  isperf2  19419  cnntr  19542  ist1-3  19616  perfcls  19632  cmpfi  19674  iscon2  19681  dfcon2  19686  snfil  20100  filcon  20119  ufileu  20155  alexsubALTlem4  20285  metequiv  20747  shlesb1i  25980  shle0  26036  orthin  26040  chcon2i  26058  chcon3i  26060  chlejb1i  26070  chabs2  26111  h1datomi  26175  cmbr4i  26195  osumcor2i  26238  pjjsi  26294  pjin2i  26788  stcltr2i  26870  mdbr2  26891  dmdbr2  26898  mdsl2i  26917  mdsl2bi  26918  mdslmd3i  26927  chrelat4i  26968  sumdmdlem2  27014  dmdbr5ati  27017  eqrelrd2  27140  dfon2lem9  28800  wfrlem8  28927  idsset  29117  fneval  29759  equivtotbnd  29877  heiborlem10  29919  isnacs2  30242  mrefg3  30244  icoiccdif  31128  cncfiooicclem1  31232  pmap11  34558  dia11N  35845  dia2dimlem5  35865  dib11N  35957  dih11  36062  dihglblem6  36137  doch11  36170  mapd11  36436  mapdcnv11N  36456
  Copyright terms: Public domain W3C validator