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

Theorem eqss 3501
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 1684 . 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 2434 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3475 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3475 . . 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 1379    = wceq 1381    e. wcel 1802    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  eqssi  3502  eqssd  3503  sseq1  3507  sseq2  3508  eqimss  3538  ssrabeq  3568  dfpss3  3572  uneqin  3731  ss0b  3797  vss  3845  pssdifn0  3870  pwpw0  4159  sssn  4169  ssunsn  4171  pwsnALT  4225  unidif  4264  ssunieq  4265  uniintsn  4305  iuneq1  4325  iuneq2  4328  iunxdif2  4359  ssext  4688  pweqb  4690  eqopab2b  4763  pwun  4774  soeq2  4806  ordtri4  4901  oneqmini  4915  eqrel  5078  eqrelrel  5090  coeq1  5146  coeq2  5147  cnveq  5162  dmeq  5189  relssres  5297  xp11  5428  ssrnres  5431  fnres  5683  eqfnfv3  5964  fneqeql2  5977  dff3  6025  fconst4  6117  f1imaeq  6154  eqoprab2b  6336  iunpw  6595  orduniorsuc  6646  tfi  6669  fo1stres  6805  fo2ndres  6806  tz7.49  7108  oawordeulem  7201  nnacan  7275  nnmcan  7281  ixpeq2  7481  sbthlem3  7627  isinf  7731  ordunifi  7768  inficl  7883  rankr1c  8237  rankc1  8286  iscard  8354  iscard2  8355  carden2  8366  aleph11  8463  cardaleph  8468  alephinit  8474  dfac12a  8526  cflm  8628  cfslb2n  8646  dfacfin7  8777  wrdeq  12538  isumltss  13634  rpnnen2  13831  isprm2  14097  mrcidb2  14887  iscyggen2  16753  iscyg3  16758  lssle0  17464  islpir2  17767  iscss2  18584  ishil2  18617  bastop1  19361  epttop  19376  iscld4  19432  0ntr  19438  opnneiid  19493  isperf2  19519  cnntr  19642  ist1-3  19716  perfcls  19732  cmpfi  19774  iscon2  19781  dfcon2  19786  snfil  20231  filcon  20250  ufileu  20286  alexsubALTlem4  20416  metequiv  20878  shlesb1i  26169  shle0  26225  orthin  26229  chcon2i  26247  chcon3i  26249  chlejb1i  26259  chabs2  26300  h1datomi  26364  cmbr4i  26384  osumcor2i  26427  pjjsi  26483  pjin2i  26977  stcltr2i  27059  mdbr2  27080  dmdbr2  27087  mdsl2i  27106  mdsl2bi  27107  mdslmd3i  27116  chrelat4i  27157  sumdmdlem2  27203  dmdbr5ati  27206  eqrelrd2  27332  dfon2lem9  29191  wfrlem8  29318  idsset  29508  fneval  30138  equivtotbnd  30242  heiborlem10  30284  isnacs2  30606  mrefg3  30608  pmap11  35188  dia11N  36477  dia2dimlem5  36497  dib11N  36589  dih11  36694  dihglblem6  36769  doch11  36802  mapd11  37068  mapdcnv11N  37088
  Copyright terms: Public domain W3C validator