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

Theorem eqss 3115
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
StepHypRef Expression
1 albiim 1612 . 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 2247 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3092 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3092 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 681 . 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 270 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    = wceq 1619    e. wcel 1621    C_ wss 3078
This theorem is referenced by:  eqssi  3116  eqssd  3117  sseq1  3120  sseq2  3121  eqimss  3151  dfpss3  3183  uneqin  3327  ss0b  3391  vss  3398  pssdifn0  3422  pwpw0  3663  sssn  3672  ssunsn  3674  pwsnALT  3722  unidif  3757  ssunieq  3758  uniintsn  3797  iuneq1  3816  iuneq2  3819  iunxdif2  3848  ssext  4122  pweqb  4124  eqopab2b  4187  pwun  4195  soeq2  4227  ordtri4  4322  oneqmini  4336  iunpw  4461  orduniorsuc  4512  tfi  4535  eqrel  4684  eqrelrel  4695  coeq1  4748  coeq2  4749  cnveq  4762  dmeq  4786  relssres  4899  xp11  5018  ssrnres  5023  fnres  5217  eqfnfv3  5476  fneqeql2  5486  dff3  5525  fconst4  5588  f1imaeq  5641  eqoprab2b  5758  fo1stres  5995  fo2ndres  5996  tz7.49  6343  oawordeulem  6438  nnacan  6512  nnmcan  6518  ixpeq2  6716  sbthlem3  6858  isinf  6961  ordunifi  6992  inficl  7062  rankr1c  7377  rankc1  7426  iscard  7492  iscard2  7493  carden2  7504  aleph11  7595  cardaleph  7600  alephinit  7606  dfac12a  7658  cflm  7760  cfslb2n  7778  dfacfin7  7909  wrdeq  11301  isumltss  12181  rpnnen2  12378  isprm2  12640  mrcidb2  13392  iscyggen2  15003  iscyg3  15008  lssle0  15542  islpir2  15835  iscss2  16418  ishil2  16451  bastop1  16563  epttop  16578  iscld4  16634  0ntr  16640  opnneiid  16695  isperf2  16715  cnntr  16836  ist1-3  16909  perfcls  16925  cmpfi  16967  iscon2  16972  dfcon2  16977  snfil  17391  filcon  17410  ufileu  17446  alexsubALTlem4  17576  metequiv  17887  shlesb1i  21795  shle0  21851  orthin  21855  chcon2i  21873  chcon3i  21875  chlejb1i  21885  chabs2  21926  h1datomi  21990  cmbr4i  22028  osumcor2i  22071  pjjsi  22127  pjin2i  22603  stcltr2i  22685  mdbr2  22706  dmdbr2  22713  mdsl2i  22732  mdsl2bi  22733  mdslmd3i  22742  chrelat4i  22783  sumdmdlem2  22829  dmdbr5ati  22832  dfon2lem9  23315  wfrlem8  23431  idsset  23605  domfldrefc  24222  ranfldrefc  24223  domintrefb  24228  twsymr  24243  sssu  24307  inposet  24444  dfps2  24455  hdrmp  24872  fneval  25453  equivtotbnd  25668  heiborlem10  25710  isnacs2  25947  mrefg3  25949  pmap11  28640  dia11N  29927  dia2dimlem5  29947  dib11N  30039  dih11  30144  dihglblem6  30219  doch11  30252  mapd11  30518  mapdcnv11N  30538
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator