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

Theorem eqss 3474
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 1666 . 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 2445 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3448 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3448 . . 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 1368    = wceq 1370    e. wcel 1758    C_ wss 3431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3438  df-ss 3445
This theorem is referenced by:  eqssi  3475  eqssd  3476  sseq1  3480  sseq2  3481  eqimss  3511  ssrabeq  3541  dfpss3  3545  uneqin  3704  ss0b  3770  vss  3818  pssdifn0  3843  pwpw0  4124  sssn  4134  ssunsn  4136  pwsnALT  4189  unidif  4228  ssunieq  4229  uniintsn  4268  iuneq1  4287  iuneq2  4290  iunxdif2  4321  ssext  4650  pweqb  4652  eqopab2b  4721  pwun  4732  soeq2  4764  ordtri4  4859  oneqmini  4873  eqrel  5032  eqrelrel  5044  coeq1  5100  coeq2  5101  cnveq  5116  dmeq  5143  relssres  5250  xp11  5376  ssrnres  5379  fnres  5630  eqfnfv3  5903  fneqeql2  5916  dff3  5960  fconst4  6046  f1imaeq  6082  eqoprab2b  6248  iunpw  6495  orduniorsuc  6546  tfi  6569  fo1stres  6705  fo2ndres  6706  tz7.49  7005  oawordeulem  7098  nnacan  7172  nnmcan  7178  ixpeq2  7382  sbthlem3  7528  isinf  7632  ordunifi  7668  inficl  7781  rankr1c  8134  rankc1  8183  iscard  8251  iscard2  8252  carden2  8263  aleph11  8360  cardaleph  8365  alephinit  8371  dfac12a  8423  cflm  8525  cfslb2n  8543  dfacfin7  8674  wrdeq  12364  isumltss  13424  rpnnen2  13621  isprm2  13884  mrcidb2  14670  iscyggen2  16474  iscyg3  16479  lssle0  17149  islpir2  17451  iscss2  18231  ishil2  18264  bastop1  18725  epttop  18740  iscld4  18796  0ntr  18802  opnneiid  18857  isperf2  18883  cnntr  19006  ist1-3  19080  perfcls  19096  cmpfi  19138  iscon2  19145  dfcon2  19150  snfil  19564  filcon  19583  ufileu  19619  alexsubALTlem4  19749  metequiv  20211  shlesb1i  24936  shle0  24992  orthin  24996  chcon2i  25014  chcon3i  25016  chlejb1i  25026  chabs2  25067  h1datomi  25131  cmbr4i  25151  osumcor2i  25194  pjjsi  25250  pjin2i  25744  stcltr2i  25826  mdbr2  25847  dmdbr2  25854  mdsl2i  25873  mdsl2bi  25874  mdslmd3i  25883  chrelat4i  25924  sumdmdlem2  25970  dmdbr5ati  25973  eqrelrd2  26092  dfon2lem9  27743  wfrlem8  27870  idsset  28060  fneval  28702  equivtotbnd  28820  heiborlem10  28862  isnacs2  29185  mrefg3  29187  pmap11  33725  dia11N  35012  dia2dimlem5  35032  dib11N  35124  dih11  35229  dihglblem6  35304  doch11  35337  mapd11  35603  mapdcnv11N  35623
  Copyright terms: Public domain W3C validator