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

Theorem eqimss2 3975
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
Assertion
Ref Expression
eqimss2 (𝐵 = 𝐴𝐴𝐵)

Proof of Theorem eqimss2
StepHypRef Expression
1 eqimss 3974 . 2 (𝐴 = 𝐵𝐴𝐵)
21eqcoms 2809 1 (𝐵 = 𝐴𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  pweq  4516  ifpprsnss  4663  unieq  4814  disjeq2  5002  disjeq1  5005  poeq2  5446  freq2  5494  seeq1  5495  seeq2  5496  dmcoeq  5814  xp11  6003  suc11  6266  funeq  6348  fimadmfoALT  6580  fconst3  6957  sorpssuni  7442  sorpssint  7443  tposeq  7881  oaass  8174  odi  8192  oen0  8199  inficl  8877  fodomfi2  9475  zorng  9919  rlimclim  14899  imasaddfnlem  16797  imasvscafn  16806  gasubg  18428  pgpssslw  18735  dprddisj2  19158  dprd2da  19161  evlslem6  20757  topgele  21539  topontopn  21549  connima  22034  islocfin  22126  ptbasfi  22190  txdis  22241  neifil  22489  elfm3  22559  rnelfmlem  22561  alexsubALTlem3  22658  alexsubALTlem4  22659  utopsnneiplem  22857  lmclimf  23912  uniiccdif  24186  dv11cn  24608  plypf1  24813  2pthon3v  27733  hstoh  30019  dmdi2  30091  disjeq1f  30340  eulerpartlemd  31738  rrvdmss  31821  umgr2cycllem  32501  refssfne  33820  neibastop3  33824  topmeet  33826  topjoin  33827  fnemeet2  33829  fnejoin1  33830  bj-restuni  34513  bj-inexeqex  34570  bj-idreseq  34578  heiborlem3  35250  funALTVeq  36092  disjeq  36126  lsatelbN  36301  lkrscss  36393  lshpset2N  36414  mapdrvallem2  38940  hdmaprnlem3eN  39153  hdmaplkr  39208  uneqsn  40723  ssrecnpr  41009  founiiun  41800  founiiun0  41814  caragendifcl  43150  imasetpreimafvbijlemfo  43919
  Copyright terms: Public domain W3C validator