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

Theorem eqss 3207
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 1601 . 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 2290 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3182 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3182 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 678 . 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 268 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  eqssi  3208  eqssd  3209  sseq1  3212  sseq2  3213  eqimss  3243  dfpss3  3275  uneqin  3433  ss0b  3497  vss  3504  pssdifn0  3528  pwpw0  3779  sssn  3788  ssunsn  3790  pwsnALT  3838  unidif  3875  ssunieq  3876  uniintsn  3915  iuneq1  3934  iuneq2  3937  iunxdif2  3966  ssext  4244  pweqb  4246  eqopab2b  4310  pwun  4318  soeq2  4350  ordtri4  4445  oneqmini  4459  iunpw  4586  orduniorsuc  4637  tfi  4660  eqrel  4793  eqrelrel  4804  coeq1  4857  coeq2  4858  cnveq  4871  dmeq  4895  relssres  5008  xp11  5127  ssrnres  5132  fnres  5376  eqfnfv3  5640  fneqeql2  5650  dff3  5689  fconst4  5752  f1imaeq  5805  eqoprab2b  5922  fo1stres  6159  fo2ndres  6160  tz7.49  6473  oawordeulem  6568  nnacan  6642  nnmcan  6648  ixpeq2  6846  sbthlem3  6989  isinf  7092  ordunifi  7123  inficl  7194  rankr1c  7509  rankc1  7558  iscard  7624  iscard2  7625  carden2  7636  aleph11  7727  cardaleph  7732  alephinit  7738  dfac12a  7790  cflm  7892  cfslb2n  7910  dfacfin7  8041  wrdeq  11440  isumltss  12323  rpnnen2  12520  isprm2  12782  mrcidb2  13536  iscyggen2  15184  iscyg3  15189  lssle0  15723  islpir2  16019  iscss2  16602  ishil2  16635  bastop1  16747  epttop  16762  iscld4  16818  0ntr  16824  opnneiid  16879  isperf2  16899  cnntr  17020  ist1-3  17093  perfcls  17109  cmpfi  17151  iscon2  17156  dfcon2  17161  snfil  17575  filcon  17594  ufileu  17630  alexsubALTlem4  17760  metequiv  18071  shlesb1i  21981  shle0  22037  orthin  22041  chcon2i  22059  chcon3i  22061  chlejb1i  22071  chabs2  22112  h1datomi  22176  cmbr4i  22196  osumcor2i  22239  pjjsi  22295  pjin2i  22789  stcltr2i  22871  mdbr2  22892  dmdbr2  22899  mdsl2i  22918  mdsl2bi  22919  mdslmd3i  22928  chrelat4i  22969  sumdmdlem2  23015  dmdbr5ati  23018  dfon2lem9  24218  wfrlem8  24334  idsset  24501  domfldrefc  25160  ranfldrefc  25161  domintrefb  25166  twsymr  25181  sssu  25244  inposet  25381  dfps2  25392  hdrmp  25809  fneval  26390  equivtotbnd  26605  heiborlem10  26647  isnacs2  26884  mrefg3  26886  pmap11  30573  dia11N  31860  dia2dimlem5  31880  dib11N  31972  dih11  32077  dihglblem6  32152  doch11  32185  mapd11  32451  mapdcnv11N  32471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator