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

Theorem eqimss2 3233
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 3232 . 2  |-  ( A  =  B  ->  A  C_  B )
21eqcoms 2288 1  |-  ( B  =  A  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    C_ wss 3154
This theorem is referenced by:  disjeq2  3999  disjeq1  4002  poeq2  4320  freq2  4366  seeq1  4367  seeq2  4368  suc11  4498  dmcoeq  4949  xp11  5113  funeq  5276  fconst3  5737  tposeq  6238  sorpssuni  6288  sorpssint  6289  oaass  6561  odi  6579  oen0  6586  inficl  7180  cantnfp1lem1  7382  cantnfp1lem3  7384  cantnflem1d  7392  cantnflem1  7393  fodomfi2  7689  zorng  8133  rlimclim  12022  imasaddfnlem  13432  imasvscafn  13441  gasubg  14758  pgpssslw  14927  dprddisj2  15276  dprd2da  15279  ply1coe  16370  frgpcyg  16529  topgele  16674  topontopn  16682  toponmre  16832  conima  17153  ptbasfi  17278  txdis  17328  neifil  17577  elfm3  17647  rnelfmlem  17649  alexsubALTlem3  17745  alexsubALTlem4  17746  lmclimf  18731  uniiccdif  18935  dv11cn  19350  evlslem6  19399  plypf1  19596  subgores  20973  hstoh  22814  dmdi2  22886  rrvdmss  23654  dfps2  25300  basexre  25533  refssfne  26305  islocfin  26307  neibastop3  26322  topmeet  26324  topjoin  26325  fnemeet2  26327  fnejoin1  26328  heiborlem3  26548  uvcresum  27253  ssrecnpr  27548  lsatelbN  29269  lkrscss  29361  lshpset2N  29382  mapdrvallem2  31908  hdmaprnlem3eN  32124  hdmaplkr  32179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator