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

Theorem eqimss2 3556
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
Assertion
Ref Expression
eqimss2

Proof of Theorem eqimss2
StepHypRef Expression
1 eqimss 3555 . 2
21eqcoms 2469 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  disjeq2  4426  disjeq1  4429  poeq2  4809  freq2  4855  seeq1  4856  seeq2  4857  suc11  4986  dmcoeq  5270  xp11  5447  funeq  5612  fconst3  6135  sorpssuni  6589  sorpssint  6590  tposeq  6976  oaass  7229  odi  7247  oen0  7254  inficl  7905  cantnfp1lem1  8118  cantnflem1  8129  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  fodomfi2  8462  zorng  8905  rlimclim  13369  imasaddfnlem  14925  imasvscafn  14934  gasubg  16340  pgpssslw  16634  dprddisj2  17087  dprddisj2OLD  17088  dprd2da  17091  evlslem6  18181  evlslem6OLD  18182  topgele  19435  topontopn  19443  toponmre  19594  conima  19926  islocfin  20018  ptbasfi  20082  txdis  20133  neifil  20381  elfm3  20451  rnelfmlem  20453  alexsubALTlem3  20549  alexsubALTlem4  20550  utopsnneiplem  20750  lmclimf  21742  uniiccdif  21987  dv11cn  22402  plypf1  22609  subgores  25306  hstoh  27151  dmdi2  27223  eulerpartlemd  28305  rrvdmss  28388  refssfne  30176  neibastop3  30180  topmeet  30182  topjoin  30183  fnemeet2  30185  fnejoin1  30186  heiborlem3  30309  ssrecnpr  31188  lsatelbN  34731  lkrscss  34823  lshpset2N  34844  mapdrvallem2  37372  hdmaprnlem3eN  37588  hdmaplkr  37643
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