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

Theorem eqimss 3555
Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
eqimss

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 3518 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  eqimss2  3556  sspss  3602  uneqin  3748  uneqdifeq  3916  pwpw0  4178  sssn  4188  eqsn  4191  snsspw  4201  pwsnALT  4244  unissint  4311  elpwuni  4418  disjeq2  4426  disjeq1  4429  pwne  4618  pwssun  4791  poeq2  4809  freq2  4855  seeq1  4856  seeq2  4857  trsucss  4968  suc11  4986  frsn  5075  dmxpss  5443  xp11  5447  dmsnopss  5485  iotassuni  5572  funeq  5612  fnresdm  5695  fssxp  5748  ffdm  5750  fcoi1  5764  fof  5800  dff1o2  5826  fvmptss  5964  fvmptss2  5975  funressn  6084  dff1o6  6181  suceloni  6648  tposeq  6976  tfrlem11  7076  oewordi  7259  oewordri  7260  dffi3  7911  cantnfle  8111  cantnflem2  8130  cantnfleOLD  8141  r1ord3g  8218  rankeq0b  8299  rankxplim3  8320  carddom2  8379  cflm  8651  cfsuc  8658  isf32lem2  8755  axdc3lem2  8852  ttukeylem5  8914  tsksuc  9161  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  invf  15162  sscres  15192  pgpssslw  16634  fislw  16645  frgpup1  16793  frgpup3lem  16795  dprdspan  17074  dprdz  17077  dprdf1o  17079  dprd2da  17091  ablfac1b  17121  lspsncmp  17762  lspsnne2  17764  lspsneq  17768  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbaglefi  18023  psrbaglefiOLD  18024  mplcoe5  18131  mplcoe2OLD  18133  mplbas2  18134  mplbas2OLD  18135  psgnghm2  18617  ofco2  18953  istps2OLD  19422  cncnpi  19779  hauscmplem  19906  iskgen2  20049  elqtop3  20204  qtoprest  20218  hmeores  20272  snfil  20365  uffixfr  20424  ustuqtop2  20745  tngngp2  21166  metnrmlem3  21365  volcn  22015  recnprss  22308  plyeq0  22608  chsupsn  26331  chlejb1i  26394  atsseq  27266  difneqnul  27415  measxun2  28181  measssd  28186  measiuns  28188  eulerpartlemb  28307  funsseq  29199  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  opnbnd  30143  cldbnd  30144  fnemeet1  30184  heiborlem10  30316  smprngopr  30449  nacsfix  30644  dvconstbi  31239  icccncfext  31690  dvmptconst  31710  dvmptidg  31712  dvmulcncf  31722  dvdivcncf  31724  dirkercncflem2  31886  fourierdlem70  31959  fourierdlem71  31960  bnj1143  33849  bnj1322  33881  lshpcmp  34713  lsatcmp  34728  lsatcmp2  34729  lshpset2N  34844  paddasslem17  35560  pcl0bN  35647  pexmidALTN  35702  lcfrlem26  37295  lcfrlem36  37305  mapd0  37392  xptrrel  37775
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