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

Theorem eqss 3518
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.)
Assertion
Ref Expression
eqss

Proof of Theorem eqss
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 albiim 1699 . 2
2 dfcleq 2450 . 2
3 dfss2 3492 . . 3
4 dfss2 3492 . . 3
53, 4anbi12i 697 . 2
61, 2, 53bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  C_wss 3475
This theorem is referenced by:  eqssi  3519  eqssd  3520  sseq1  3524  sseq2  3525  eqimss  3555  ssrabeq  3585  dfpss3  3589  uneqin  3748  ss0b  3815  vss  3863  pssdifn0  3888  pwpw0  4178  sssn  4188  ssunsn  4190  pwsnALT  4244  unidif  4283  ssunieq  4284  uniintsn  4324  iuneq1  4344  iuneq2  4347  iunxdif2  4378  ssext  4707  pweqb  4709  eqopab2b  4782  pwun  4793  soeq2  4825  ordtri4  4920  oneqmini  4934  eqrel  5097  eqrelrel  5109  coeq1  5165  coeq2  5166  cnveq  5181  dmeq  5208  relssres  5316  xp11  5447  ssrnres  5450  fnres  5702  eqfnfv3  5983  fneqeql2  5996  dff3  6044  fconst4  6136  f1imaeq  6173  eqoprab2b  6355  iunpw  6614  orduniorsuc  6665  tfi  6688  fo1stres  6824  fo2ndres  6825  tz7.49  7129  oawordeulem  7222  nnacan  7296  nnmcan  7302  ixpeq2  7503  sbthlem3  7649  isinf  7753  ordunifi  7790  inficl  7905  rankr1c  8260  rankc1  8309  iscard  8377  iscard2  8378  carden2  8389  aleph11  8486  cardaleph  8491  alephinit  8497  dfac12a  8549  cflm  8651  cfslb2n  8669  dfacfin7  8800  wrdeq  12564  isumltss  13660  rpnnen2  13959  isprm2  14225  mrcidb2  15015  iscyggen2  16884  iscyg3  16889  lssle0  17596  islpir2  17899  iscss2  18717  ishil2  18750  bastop1  19495  epttop  19510  iscld4  19566  0ntr  19572  opnneiid  19627  isperf2  19653  cnntr  19776  ist1-3  19850  perfcls  19866  cmpfi  19908  iscon2  19915  dfcon2  19920  snfil  20365  filcon  20384  ufileu  20420  alexsubALTlem4  20550  metequiv  21012  shlesb1i  26304  shle0  26360  orthin  26364  chcon2i  26382  chcon3i  26384  chlejb1i  26394  chabs2  26435  h1datomi  26499  cmbr4i  26519  osumcor2i  26562  pjjsi  26618  pjin2i  27112  stcltr2i  27194  mdbr2  27215  dmdbr2  27222  mdsl2i  27241  mdsl2bi  27242  mdslmd3i  27251  chrelat4i  27292  sumdmdlem2  27338  dmdbr5ati  27341  eqrelrd2  27467  dfon2lem9  29223  wfrlem8  29350  idsset  29540  fneval  30170  equivtotbnd  30274  heiborlem10  30316  isnacs2  30638  mrefg3  30640  pmap11  35486  dia11N  36775  dia2dimlem5  36795  dib11N  36887  dih11  36992  dihglblem6  37067  doch11  37100  mapd11  37366  mapdcnv11N  37386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator