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

Theorem eqimss2 3244
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
Assertion
Ref Expression
eqimss2  |-  ( B  =  A  ->  A  C_  B )

Proof of Theorem eqimss2
StepHypRef Expression
1 eqimss 3243 . 2  |-  ( A  =  B  ->  A  C_  B )
21eqcoms 2299 1  |-  ( B  =  A  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  disjeq2  4013  disjeq1  4016  poeq2  4334  freq2  4380  seeq1  4381  seeq2  4382  suc11  4512  dmcoeq  4963  xp11  5127  funeq  5290  fconst3  5751  tposeq  6252  sorpssuni  6302  sorpssint  6303  oaass  6575  odi  6593  oen0  6600  inficl  7194  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnflem1d  7406  cantnflem1  7407  fodomfi2  7703  zorng  8147  rlimclim  12036  imasaddfnlem  13446  imasvscafn  13455  gasubg  14772  pgpssslw  14941  dprddisj2  15290  dprd2da  15293  ply1coe  16384  frgpcyg  16543  topgele  16688  topontopn  16696  toponmre  16846  conima  17167  ptbasfi  17292  txdis  17342  neifil  17591  elfm3  17661  rnelfmlem  17663  alexsubALTlem3  17759  alexsubALTlem4  17760  lmclimf  18745  uniiccdif  18949  dv11cn  19364  evlslem6  19413  plypf1  19610  subgores  20987  hstoh  22828  dmdi2  22900  rrvdmss  23667  dfps2  25392  basexre  25625  refssfne  26397  islocfin  26399  neibastop3  26414  topmeet  26416  topjoin  26417  fnemeet2  26419  fnejoin1  26420  heiborlem3  26640  uvcresum  27345  ssrecnpr  27640  lsatelbN  29818  lkrscss  29910  lshpset2N  29931  mapdrvallem2  32457  hdmaprnlem3eN  32673  hdmaplkr  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator