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

Theorem eqimss2 3393
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 3392 . 2  |-  ( A  =  B  ->  A  C_  B )
21eqcoms 2438 1  |-  ( B  =  A  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  disjeq2  4178  disjeq1  4181  poeq2  4499  freq2  4545  seeq1  4546  seeq2  4547  suc11  4677  dmcoeq  5130  xp11  5296  funeq  5465  fconst3  5947  tposeq  6473  sorpssuni  6523  sorpssint  6524  oaass  6796  odi  6814  oen0  6821  inficl  7422  cantnfp1lem1  7626  cantnfp1lem3  7628  cantnflem1d  7636  cantnflem1  7637  fodomfi2  7933  zorng  8376  rlimclim  12332  imasaddfnlem  13745  imasvscafn  13754  gasubg  15071  pgpssslw  15240  dprddisj2  15589  dprd2da  15592  ply1coe  16676  frgpcyg  16846  topgele  16991  topontopn  16999  toponmre  17149  conima  17480  ptbasfi  17605  txdis  17656  neifil  17904  elfm3  17974  rnelfmlem  17976  alexsubALTlem3  18072  alexsubALTlem4  18073  utopsnneiplem  18269  lmclimf  19248  uniiccdif  19462  dv11cn  19877  evlslem6  19926  plypf1  20123  subgores  21884  hstoh  23727  dmdi2  23799  rrvdmss  24699  refssfne  26365  islocfin  26367  neibastop3  26382  topmeet  26384  topjoin  26385  fnemeet2  26387  fnejoin1  26388  heiborlem3  26513  uvcresum  27210  ssrecnpr  27505  lsatelbN  29741  lkrscss  29833  lshpset2N  29854  mapdrvallem2  32380  hdmaprnlem3eN  32596  hdmaplkr  32651
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator