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

Theorem eqss 3504
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 1704 . 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 2447 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3478 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3478 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 695 . 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 367   A.wal 1396    = wceq 1398    e. wcel 1823    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  eqssi  3505  eqssd  3506  sseq1  3510  sseq2  3511  eqimss  3541  ssrabeq  3572  dfpss3  3576  uneqin  3746  ss0b  3814  vss  3851  pssdifn0  3876  pwpw0  4164  sssn  4174  ssunsn  4176  pwsnALT  4230  unidif  4268  ssunieq  4269  uniintsn  4309  iuneq1  4329  iuneq2  4332  iunxdif2  4363  ssext  4692  pweqb  4694  eqopab2b  4766  pwun  4777  soeq2  4809  ordtri4  4904  oneqmini  4918  eqrel  5080  eqrelrel  5092  coeq1  5149  coeq2  5150  cnveq  5165  dmeq  5192  relssres  5299  xp11  5427  ssrnres  5430  fnres  5679  eqfnfv3  5959  fneqeql2  5972  dff3  6020  fconst4  6111  f1imaeq  6148  eqoprab2b  6328  iunpw  6587  orduniorsuc  6638  tfi  6661  fo1stres  6797  fo2ndres  6798  tz7.49  7102  oawordeulem  7195  nnacan  7269  nnmcan  7275  ixpeq2  7476  sbthlem3  7622  isinf  7726  ordunifi  7762  inficl  7877  rankr1c  8230  rankc1  8279  iscard  8347  iscard2  8348  carden2  8359  aleph11  8456  cardaleph  8461  alephinit  8467  dfac12a  8519  cflm  8621  cfslb2n  8639  dfacfin7  8770  wrdeq  12554  isumltss  13745  rpnnen2  14046  isprm2  14312  mrcidb2  15110  iscyggen2  17086  iscyg3  17091  lssle0  17794  islpir2  18097  iscss2  18893  ishil2  18926  bastop1  19665  epttop  19680  iscld4  19736  0ntr  19742  opnneiid  19797  isperf2  19823  cnntr  19946  ist1-3  20020  perfcls  20036  cmpfi  20078  iscon2  20084  dfcon2  20089  snfil  20534  filcon  20553  ufileu  20589  alexsubALTlem4  20719  metequiv  21181  shlesb1i  26505  shle0  26561  orthin  26565  chcon2i  26583  chcon3i  26585  chlejb1i  26595  chabs2  26636  h1datomi  26700  cmbr4i  26720  osumcor2i  26763  pjjsi  26819  pjin2i  27313  stcltr2i  27395  mdbr2  27416  dmdbr2  27423  mdsl2i  27442  mdsl2bi  27443  mdslmd3i  27452  chrelat4i  27493  sumdmdlem2  27539  dmdbr5ati  27542  eqrelrd2  27685  dfon2lem9  29466  wfrlem8  29593  idsset  29771  fneval  30413  equivtotbnd  30517  heiborlem10  30559  isnacs2  30881  mrefg3  30883  pmap11  35902  dia11N  37191  dia2dimlem5  37211  dib11N  37303  dih11  37408  dihglblem6  37483  doch11  37516  mapd11  37782  mapdcnv11N  37802
  Copyright terms: Public domain W3C validator