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

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

Proof of Theorem eqimss2
StepHypRef Expression
1 eqimss 4020 . 2 (𝐴 = 𝐵𝐴𝐵)
21eqcoms 2826 1 (𝐵 = 𝐴𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  ifpprsnss  4692  disjeq2  5026  disjeq1  5029  poeq2  5471  freq2  5519  seeq1  5520  seeq2  5521  dmcoeq  5838  xp11  6025  suc11  6287  funeq  6368  fimadmfoALT  6594  fconst3  6967  sorpssuni  7447  sorpssint  7448  tposeq  7883  oaass  8176  odi  8194  oen0  8201  inficl  8877  fodomfi2  9474  zorng  9914  rlimclim  14891  imasaddfnlem  16789  imasvscafn  16798  gasubg  18370  pgpssslw  18668  dprddisj2  19090  dprd2da  19093  evlslem6  20222  topgele  21466  topontopn  21476  connima  21961  islocfin  22053  ptbasfi  22117  txdis  22168  neifil  22416  elfm3  22486  rnelfmlem  22488  alexsubALTlem3  22585  alexsubALTlem4  22586  utopsnneiplem  22783  lmclimf  23834  uniiccdif  24106  dv11cn  24525  plypf1  24729  2pthon3v  27649  hstoh  29936  dmdi2  30008  disjeq1f  30251  eulerpartlemd  31523  rrvdmss  31606  umgr2cycllem  32284  refssfne  33603  neibastop3  33607  topmeet  33609  topjoin  33610  fnemeet2  33612  fnejoin1  33613  bj-restuni  34282  bj-inexeqex  34338  bj-idreseq  34346  heiborlem3  34972  funALTVeq  35813  disjeq  35847  lsatelbN  36022  lkrscss  36114  lshpset2N  36135  mapdrvallem2  38661  hdmaprnlem3eN  38874  hdmaplkr  38929  uneqsn  40251  ssrecnpr  40517  founiiun  41311  founiiun0  41327  caragendifcl  42673  imasetpreimafvbijlemfo  43442
  Copyright terms: Public domain W3C validator