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

Theorem eqimss 3620
Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
eqimss (𝐴 = 𝐵𝐴𝐵)

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 3583 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 475 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  eqimss2  3621  sspss  3668  uneqin  3837  difn0  3897  ssdisj  3978  uneqdifeq  4009  uneqdifeqOLD  4010  pwpw0  4284  sssn  4296  eqsnOLD  4300  snsspw  4311  pwsnALT  4362  unissint  4431  elpwuni  4544  disjeq2  4552  disjeq1  4555  pwne  4752  pwssun  4934  poeq2  4953  freq2  4999  seeq1  5000  seeq2  5001  frsn  5102  dmxpss  5470  xp11  5474  dmsnopss  5511  trsucss  5714  suc11  5734  iotassuni  5770  funeq  5809  fnresdm  5900  fssxp  5959  ffdm  5961  fcoi1  5976  fof  6013  dff1o2  6040  fvmptss  6186  fvmptss2  6197  funressn  6309  dff1o6  6409  suceloni  6883  tposeq  7219  tfrlem11  7349  oewordi  7536  oewordri  7537  dffi3  8198  cantnfle  8429  cantnflem2  8448  r1ord3g  8503  rankeq0b  8584  rankxplim3  8605  carddom2  8664  cflm  8933  cfsuc  8940  isf32lem2  9037  axdc3lem2  9134  ttukeylem5  9196  tsksuc  9441  fsuppmapnn0fiublem  12609  fsuppmapnn0fiub  12610  fsuppmapnn0fiubOLD  12611  xptrrel  13516  relexpnndm  13578  relexpdmg  13579  relexprng  13583  relexpfld  13586  relexpaddg  13590  invf  16200  sscres  16255  pgpssslw  17801  fislw  17812  frgpup1  17960  frgpup3lem  17962  dprdspan  18198  dprdz  18201  dprdf1o  18203  dprd2da  18213  ablfac1b  18241  lspsncmp  18886  lspsnne2  18888  lspsneq  18892  psrbaglesupp  19138  psrbaglefi  19142  mplcoe5  19238  mplbas2  19240  psgnghm2  19694  ofco2  20024  cncnpi  20840  hauscmplem  20967  iskgen2  21109  elqtop3  21264  qtoprest  21278  hmeores  21332  snfil  21426  uffixfr  21485  ustuqtop2  21804  tngngp2  22214  metnrmlem3  22420  volcn  23125  recnprss  23419  plyeq0  23716  chsupsn  27450  chlejb1i  27513  atsseq  28384  disjeq1f  28563  ldgenpisys  29350  measxun2  29394  measssd  29399  measiuns  29401  pmeasmono  29507  eulerpartlemb  29551  bnj1143  29909  bnj1322  29941  funsseq  30706  opnbnd  31284  cldbnd  31285  fnemeet1  31325  bj-restuni  32025  bj-sspwpweq  32034  bj-toprntopon  32038  relowlpssretop  32182  ovoliunnfl  32415  voliunnfl  32417  volsupnfl  32418  heiborlem10  32583  smprngopr  32815  lshpcmp  33087  lsatcmp  33102  lsatcmp2  33103  lshpset2N  33218  paddasslem17  33934  pcl0bN  34021  pexmidALTN  34076  lcfrlem26  35669  lcfrlem36  35679  mapd0  35766  nacsfix  36087  cbviuneq12df  36766  relexp0a  36821  relexpaddss  36823  frege124d  36866  k0004lem3  37261  dvconstbi  37349  ssin0  38042  icccncfext  38567  dvmptconst  38597  dvmptidg  38599  dvmulcncf  38609  dvdivcncf  38611  dirkercncflem2  38791  fourierdlem70  38863  fourierdlem71  38864  hoicvr  39232  ovnsubaddlem1  39254  ovnhoi  39287  hspdifhsp  39300  ssprsseq  40119  structvtxvallem  40245  uhgr3cyclex  41341
  Copyright terms: Public domain W3C validator