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

Theorem eqimss2 3344
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 3343 . 2  |-  ( A  =  B  ->  A  C_  B )
21eqcoms 2390 1  |-  ( B  =  A  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3263
This theorem is referenced by:  disjeq2  4127  disjeq1  4130  poeq2  4448  freq2  4494  seeq1  4495  seeq2  4496  suc11  4625  dmcoeq  5078  xp11  5244  funeq  5413  fconst3  5894  tposeq  6417  sorpssuni  6467  sorpssint  6468  oaass  6740  odi  6758  oen0  6765  inficl  7365  cantnfp1lem1  7567  cantnfp1lem3  7569  cantnflem1d  7577  cantnflem1  7578  fodomfi2  7874  zorng  8317  rlimclim  12267  imasaddfnlem  13680  imasvscafn  13689  gasubg  15006  pgpssslw  15175  dprddisj2  15524  dprd2da  15527  ply1coe  16611  frgpcyg  16777  topgele  16922  topontopn  16930  toponmre  17080  conima  17409  ptbasfi  17534  txdis  17585  neifil  17833  elfm3  17903  rnelfmlem  17905  alexsubALTlem3  18001  alexsubALTlem4  18002  utopsnneiplem  18198  lmclimf  19127  uniiccdif  19337  dv11cn  19752  evlslem6  19801  plypf1  19998  subgores  21740  hstoh  23583  dmdi2  23655  rrvdmss  24486  refssfne  26065  islocfin  26067  neibastop3  26082  topmeet  26084  topjoin  26085  fnemeet2  26087  fnejoin1  26088  heiborlem3  26213  uvcresum  26911  ssrecnpr  27206  lsatelbN  29121  lkrscss  29213  lshpset2N  29234  mapdrvallem2  31760  hdmaprnlem3eN  31976  hdmaplkr  32031
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator