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

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

Proof of Theorem eqimss2
StepHypRef Expression
1 eqimss 3641 . 2 (𝐴 = 𝐵𝐴𝐵)
21eqcoms 2629 1 (𝐵 = 𝐴𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573
This theorem is referenced by:  ifpprsnss  4274  disjeq2  4592  disjeq1  4595  poeq2  5004  freq2  5050  seeq1  5051  seeq2  5052  dmcoeq  5353  xp11  5533  suc11  5795  funeq  5872  fconst3  6437  sorpssuni  6906  sorpssint  6907  tposeq  7306  oaass  7593  odi  7611  oen0  7618  inficl  8282  cantnfp1lem1  8526  cantnflem1  8537  fodomfi2  8834  zorng  9277  rlimclim  14218  imasaddfnlem  16116  imasvscafn  16125  gasubg  17663  pgpssslw  17957  dprddisj2  18366  dprd2da  18369  evlslem6  19441  topgele  20654  topontopn  20664  toponmre  20816  connima  21147  islocfin  21239  ptbasfi  21303  txdis  21354  neifil  21603  elfm3  21673  rnelfmlem  21675  alexsubALTlem3  21772  alexsubALTlem4  21773  utopsnneiplem  21970  lmclimf  23021  uniiccdif  23265  dv11cn  23681  plypf1  23885  2pthon3v  26721  hstoh  28958  dmdi2  29030  disjeq1f  29250  eulerpartlemd  30227  rrvdmss  30310  refssfne  32022  neibastop3  32026  topmeet  32028  topjoin  32029  fnemeet2  32031  fnejoin1  32032  bj-restuni  32714  heiborlem3  33271  lsatelbN  33800  lkrscss  33892  lshpset2N  33913  mapdrvallem2  36441  hdmaprnlem3eN  36657  hdmaplkr  36712  uneqsn  37830  ssrecnpr  38016  founiiun  38857  founiiun0  38874  caragendifcl  40056
  Copyright terms: Public domain W3C validator