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

Theorem eqss 3365
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 1622 . 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 2432 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3339 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3339 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 680 . 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 4    <-> wb 178    /\ wa 360   A.wal 1550    = wceq 1653    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  eqssi  3366  eqssd  3367  sseq1  3371  sseq2  3372  eqimss  3402  ssrabeq  3431  dfpss3  3435  uneqin  3594  ss0b  3659  vss  3666  pssdifn0  3691  pwpw0  3948  sssn  3959  ssunsn  3961  pwsnALT  4012  unidif  4049  ssunieq  4050  uniintsn  4089  iuneq1  4108  iuneq2  4111  iunxdif2  4141  ssext  4421  pweqb  4423  eqopab2b  4487  pwun  4494  soeq2  4526  ordtri4  4621  oneqmini  4635  iunpw  4762  orduniorsuc  4813  tfi  4836  eqrel  4968  eqrelrel  4980  coeq1  5033  coeq2  5034  cnveq  5049  dmeq  5073  relssres  5186  xp11  5307  ssrnres  5312  fnres  5564  eqfnfv3  5832  fneqeql2  5842  dff3  5885  fconst4  5959  f1imaeq  6014  eqoprab2b  6135  fo1stres  6373  fo2ndres  6374  tz7.49  6705  oawordeulem  6800  nnacan  6874  nnmcan  6880  ixpeq2  7079  sbthlem3  7222  isinf  7325  ordunifi  7360  inficl  7433  rankr1c  7750  rankc1  7799  iscard  7867  iscard2  7868  carden2  7879  aleph11  7970  cardaleph  7975  alephinit  7981  dfac12a  8033  cflm  8135  cfslb2n  8153  dfacfin7  8284  wrdeq  11743  isumltss  12633  rpnnen2  12830  isprm2  13092  mrcidb2  13848  iscyggen2  15496  iscyg3  15501  lssle0  16031  islpir2  16327  iscss2  16918  ishil2  16951  bastop1  17063  epttop  17078  iscld4  17134  0ntr  17140  opnneiid  17195  isperf2  17221  cnntr  17344  ist1-3  17418  perfcls  17434  cmpfi  17476  iscon2  17482  dfcon2  17487  snfil  17901  filcon  17920  ufileu  17956  alexsubALTlem4  18086  metequiv  18544  shlesb1i  22893  shle0  22949  orthin  22953  chcon2i  22971  chcon3i  22973  chlejb1i  22983  chabs2  23024  h1datomi  23088  cmbr4i  23108  osumcor2i  23151  pjjsi  23207  pjin2i  23701  stcltr2i  23783  mdbr2  23804  dmdbr2  23811  mdsl2i  23830  mdsl2bi  23831  mdslmd3i  23840  chrelat4i  23881  sumdmdlem2  23927  dmdbr5ati  23930  dfon2lem9  25423  wfrlem8  25550  idsset  25740  fneval  26381  equivtotbnd  26501  heiborlem10  26543  isnacs2  26774  mrefg3  26776  pmap11  30633  dia11N  31920  dia2dimlem5  31940  dib11N  32032  dih11  32137  dihglblem6  32212  doch11  32245  mapd11  32511  mapdcnv11N  32531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator