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

Theorem eqss 3169
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 2252 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3144 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3144 . . 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 3127
This theorem is referenced by:  eqssi  3170  eqssd  3171  sseq1  3174  sseq2  3175  eqimss  3205  dfpss3  3237  uneqin  3395  ss0b  3459  vss  3466  pssdifn0  3490  pwpw0  3737  sssn  3746  ssunsn  3748  pwsnALT  3796  unidif  3833  ssunieq  3834  uniintsn  3873  iuneq1  3892  iuneq2  3895  iunxdif2  3924  ssext  4200  pweqb  4202  eqopab2b  4266  pwun  4274  soeq2  4306  ordtri4  4401  oneqmini  4415  iunpw  4542  orduniorsuc  4593  tfi  4616  eqrel  4765  eqrelrel  4776  coeq1  4829  coeq2  4830  cnveq  4843  dmeq  4867  relssres  4980  xp11  5099  ssrnres  5104  fnres  5298  eqfnfv3  5558  fneqeql2  5568  dff3  5607  fconst4  5670  f1imaeq  5723  eqoprab2b  5840  fo1stres  6077  fo2ndres  6078  tz7.49  6425  oawordeulem  6520  nnacan  6594  nnmcan  6600  ixpeq2  6798  sbthlem3  6941  isinf  7044  ordunifi  7075  inficl  7146  rankr1c  7461  rankc1  7510  iscard  7576  iscard2  7577  carden2  7588  aleph11  7679  cardaleph  7684  alephinit  7690  dfac12a  7742  cflm  7844  cfslb2n  7862  dfacfin7  7993  wrdeq  11390  isumltss  12270  rpnnen2  12467  isprm2  12729  mrcidb2  13483  iscyggen2  15131  iscyg3  15136  lssle0  15670  islpir2  15966  iscss2  16549  ishil2  16582  bastop1  16694  epttop  16709  iscld4  16765  0ntr  16771  opnneiid  16826  isperf2  16846  cnntr  16967  ist1-3  17040  perfcls  17056  cmpfi  17098  iscon2  17103  dfcon2  17108  snfil  17522  filcon  17541  ufileu  17577  alexsubALTlem4  17707  metequiv  18018  shlesb1i  21926  shle0  21982  orthin  21986  chcon2i  22004  chcon3i  22006  chlejb1i  22016  chabs2  22057  h1datomi  22121  cmbr4i  22141  osumcor2i  22184  pjjsi  22240  pjin2i  22734  stcltr2i  22816  mdbr2  22837  dmdbr2  22844  mdsl2i  22863  mdsl2bi  22864  mdslmd3i  22873  chrelat4i  22914  sumdmdlem2  22960  dmdbr5ati  22963  dfon2lem9  23517  wfrlem8  23633  idsset  23807  domfldrefc  24424  ranfldrefc  24425  domintrefb  24430  twsymr  24445  sssu  24509  inposet  24646  dfps2  24657  hdrmp  25074  fneval  25655  equivtotbnd  25870  heiborlem10  25912  isnacs2  26149  mrefg3  26151  pmap11  29201  dia11N  30488  dia2dimlem5  30508  dib11N  30600  dih11  30705  dihglblem6  30780  doch11  30813  mapd11  31079  mapdcnv11N  31099
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 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator