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

Theorem eqimss2 3523
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 3522 . 2  |-  ( A  =  B  ->  A  C_  B )
21eqcoms 2441 1  |-  ( B  =  A  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  disjeq2  4401  disjeq1  4404  poeq2  4779  freq2  4825  seeq1  4826  seeq2  4827  dmcoeq  5117  xp11  5292  suc11  5545  funeq  5620  fconst3  6143  sorpssuni  6594  sorpssint  6595  tposeq  6983  oaass  7270  odi  7288  oen0  7295  inficl  7945  cantnfp1lem1  8182  cantnflem1  8193  fodomfi2  8489  zorng  8932  rlimclim  13588  imasaddfnlem  15385  imasvscafn  15394  gasubg  16907  pgpssslw  17201  dprddisj2  17607  dprd2da  17610  evlslem6  18671  topgele  19880  topontopn  19888  toponmre  20040  conima  20371  islocfin  20463  ptbasfi  20527  txdis  20578  neifil  20826  elfm3  20896  rnelfmlem  20898  alexsubALTlem3  20995  alexsubALTlem4  20996  utopsnneiplem  21193  lmclimf  22166  uniiccdif  22412  dv11cn  22830  plypf1  23034  subgores  25877  hstoh  27720  dmdi2  27792  disjeq1f  28023  eulerpartlemd  29025  rrvdmss  29108  refssfne  30799  neibastop3  30803  topmeet  30805  topjoin  30806  fnemeet2  30808  fnejoin1  30809  heiborlem3  31849  lsatelbN  32281  lkrscss  32373  lshpset2N  32394  mapdrvallem2  34922  hdmaprnlem3eN  35138  hdmaplkr  35193  ssrecnpr  36293  founiiun  37069  founiiun0  37088  caragendifcl  37844
  Copyright terms: Public domain W3C validator