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

Theorem eqss 3355
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 1621 . 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 2429 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3329 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3329 . . 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 1549    = wceq 1652    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  eqssi  3356  eqssd  3357  sseq1  3361  sseq2  3362  eqimss  3392  ssrabeq  3421  dfpss3  3425  uneqin  3584  ss0b  3649  vss  3656  pssdifn0  3681  pwpw0  3938  sssn  3949  ssunsn  3951  pwsnALT  4002  unidif  4039  ssunieq  4040  uniintsn  4079  iuneq1  4098  iuneq2  4101  iunxdif2  4131  ssext  4410  pweqb  4412  eqopab2b  4476  pwun  4483  soeq2  4515  ordtri4  4610  oneqmini  4624  iunpw  4751  orduniorsuc  4802  tfi  4825  eqrel  4957  eqrelrel  4969  coeq1  5022  coeq2  5023  cnveq  5038  dmeq  5062  relssres  5175  xp11  5296  ssrnres  5301  fnres  5553  eqfnfv3  5821  fneqeql2  5831  dff3  5874  fconst4  5948  f1imaeq  6003  eqoprab2b  6124  fo1stres  6362  fo2ndres  6363  tz7.49  6694  oawordeulem  6789  nnacan  6863  nnmcan  6869  ixpeq2  7068  sbthlem3  7211  isinf  7314  ordunifi  7349  inficl  7422  rankr1c  7739  rankc1  7788  iscard  7854  iscard2  7855  carden2  7866  aleph11  7957  cardaleph  7962  alephinit  7968  dfac12a  8020  cflm  8122  cfslb2n  8140  dfacfin7  8271  wrdeq  11730  isumltss  12620  rpnnen2  12817  isprm2  13079  mrcidb2  13835  iscyggen2  15483  iscyg3  15488  lssle0  16018  islpir2  16314  iscss2  16905  ishil2  16938  bastop1  17050  epttop  17065  iscld4  17121  0ntr  17127  opnneiid  17182  isperf2  17208  cnntr  17331  ist1-3  17405  perfcls  17421  cmpfi  17463  iscon2  17469  dfcon2  17474  snfil  17888  filcon  17907  ufileu  17943  alexsubALTlem4  18073  metequiv  18531  shlesb1i  22880  shle0  22936  orthin  22940  chcon2i  22958  chcon3i  22960  chlejb1i  22970  chabs2  23011  h1datomi  23075  cmbr4i  23095  osumcor2i  23138  pjjsi  23194  pjin2i  23688  stcltr2i  23770  mdbr2  23791  dmdbr2  23798  mdsl2i  23817  mdsl2bi  23818  mdslmd3i  23827  chrelat4i  23868  sumdmdlem2  23914  dmdbr5ati  23917  dfon2lem9  25410  wfrlem8  25537  idsset  25727  fneval  26358  equivtotbnd  26478  heiborlem10  26520  isnacs2  26751  mrefg3  26753  pmap11  30496  dia11N  31783  dia2dimlem5  31803  dib11N  31895  dih11  32000  dihglblem6  32075  doch11  32108  mapd11  32374  mapdcnv11N  32394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator