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

Theorem eqss 3415
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 1746 . 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 2416 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3389 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3389 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 701 . 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 280 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1872    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3379  df-ss 3386
This theorem is referenced by:  eqssi  3416  eqssd  3417  sseq1  3421  sseq2  3422  eqimss  3452  ssrabeq  3483  dfpss3  3487  uneqin  3660  ss0b  3730  vss  3767  pssdifn0  3793  pwpw0  4084  sssn  4094  ssunsn  4096  pwsnALT  4150  unidif  4188  ssunieq  4189  uniintsn  4229  iuneq1  4249  iuneq2  4252  iunxdif2  4283  ssext  4612  pweqb  4614  eqopab2b  4686  pwun  4697  soeq2  4730  eqrel  4879  eqrelrel  4891  coeq1  4947  coeq2  4948  cnveq  4963  dmeq  4990  relssres  5097  xp11  5227  ssrnres  5230  ordtri4  5415  oneqmini  5429  fnres  5646  eqfnfv3  5930  fneqeql2  5943  dff3  5987  fconst4  6081  f1imaeq  6118  eqoprab2b  6300  iunpw  6556  orduniorsuc  6608  tfi  6631  fo1stres  6768  fo2ndres  6769  wfrlem8  6991  tz7.49  7110  oawordeulem  7203  nnacan  7277  nnmcan  7283  ixpeq2  7484  sbthlem3  7630  isinf  7731  ordunifi  7767  inficl  7885  rankr1c  8237  rankc1  8286  iscard  8354  iscard2  8355  carden2  8366  aleph11  8459  cardaleph  8464  alephinit  8470  dfac12a  8522  cflm  8624  cfslb2n  8642  dfacfin7  8773  wrdeq  12630  isumltss  13842  rpnnen2  14214  isprm2  14568  mrcidb2  15460  iscyggen2  17452  iscyg3  17457  lssle0  18109  islpir2  18411  iscss2  19184  ishil2  19217  bastop1  19944  epttop  19959  iscld4  20016  0ntr  20022  opnneiid  20077  isperf2  20103  cnntr  20226  ist1-3  20300  perfcls  20316  cmpfi  20358  iscon2  20364  dfcon2  20369  snfil  20814  filcon  20833  ufileu  20869  alexsubALTlem4  21000  metequiv  21459  shlesb1i  26974  shle0  27030  orthin  27034  chcon2i  27052  chcon3i  27054  chlejb1i  27064  chabs2  27105  h1datomi  27169  cmbr4i  27189  osumcor2i  27232  pjjsi  27288  pjin2i  27781  stcltr2i  27863  mdbr2  27884  dmdbr2  27891  mdsl2i  27910  mdsl2bi  27911  mdslmd3i  27920  chrelat4i  27961  sumdmdlem2  28007  dmdbr5ati  28010  eqrelrd2  28161  dfon2lem9  30381  idsset  30599  fneval  30950  topdifinfeq  31654  equivtotbnd  32011  heiborlem10  32053  pmap11  33233  dia11N  34522  dia2dimlem5  34542  dib11N  34634  dih11  34739  dihglblem6  34814  doch11  34847  mapd11  35113  mapdcnv11N  35133  isnacs2  35454  mrefg3  35456  rababg  36086  relnonrel  36100  prsal  38037  nbuhgr2vtx1edgblem  39149
  Copyright terms: Public domain W3C validator