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

Theorem eqimss 3690
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 3651 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 475 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  eqimss2  3691  sspss  3739  uneqin  3911  difn0  3976  ssdisj  4059  uneqdifeq  4090  uneqdifeqOLD  4091  pwpw0  4376  ssprsseq  4389  sssn  4390  eqsnOLD  4394  snsspw  4407  pwsnALT  4461  unissint  4533  pwpwssunieq  4647  elpwuni  4648  disjeq2  4656  disjeq1  4659  pwne  4861  pwssun  5049  poeq2  5068  freq2  5114  seeq1  5115  seeq2  5116  frsn  5223  dmxpss  5600  xp11  5604  dmsnopss  5643  trsucss  5849  suc11  5869  iotassuni  5905  funeq  5946  fnresdm  6038  fssxp  6098  ffdm  6100  fcoi1  6116  fof  6153  dff1o2  6180  fvmptss  6331  fvmptss2  6343  funressn  6466  dff1o6  6571  suceloni  7055  tposeq  7399  tfrlem11  7529  oewordi  7716  oewordri  7717  dffi3  8378  cantnfle  8606  cantnflem2  8625  r1ord3g  8680  rankeq0b  8761  rankxplim3  8782  carddom2  8841  cflm  9110  cfsuc  9117  isf32lem2  9214  axdc3lem2  9311  ttukeylem5  9373  tsksuc  9622  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  xptrrel  13765  relexpnndm  13825  relexpdmg  13826  relexprng  13830  relexpfld  13833  relexpaddg  13837  invf  16475  sscres  16530  pgpssslw  18075  fislw  18086  frgpup1  18234  frgpup3lem  18236  dprdspan  18472  dprdz  18475  dprdf1o  18477  dprd2da  18487  ablfac1b  18515  lspsncmp  19164  lspsnne2  19166  lspsneq  19170  psrbaglesupp  19416  psrbaglefi  19420  mplcoe5  19516  mplbas2  19518  psgnghm2  19975  ofco2  20305  toprntopon  20777  cncnpi  21130  hauscmplem  21257  iskgen2  21399  elqtop3  21554  qtoprest  21568  hmeores  21622  snfil  21715  uffixfr  21774  ustuqtop2  22093  tngngp2  22503  metnrmlem3  22711  volcn  23420  recnprss  23713  plyeq0  24012  uhgr3cyclex  27160  chsupsn  28400  chlejb1i  28463  atsseq  29334  disjeq1f  29513  ldgenpisys  30357  measxun2  30401  measssd  30406  measiuns  30408  pmeasmono  30514  eulerpartlemb  30558  bnj1143  30987  bnj1322  31019  funsseq  31792  opnbnd  32445  cldbnd  32446  fnemeet1  32486  bj-restuni  33175  relowlpssretop  33342  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  heiborlem10  33749  smprngopr  33981  lshpcmp  34593  lsatcmp  34608  lsatcmp2  34609  lshpset2N  34724  paddasslem17  35440  pcl0bN  35527  pexmidALTN  35582  lcfrlem26  37174  lcfrlem36  37184  mapd0  37271  nacsfix  37592  cbviuneq12df  38270  relexp0a  38325  relexpaddss  38327  frege124d  38370  k0004lem3  38764  dvconstbi  38850  ssin0  39537  icccncfext  40418  dvmptconst  40447  dvmptidg  40449  dvmulcncf  40458  dvdivcncf  40460  dirkercncflem2  40639  fourierdlem70  40711  fourierdlem71  40712  hoicvr  41083  ovnsubaddlem1  41105  ovnhoi  41138  hspdifhsp  41151  0setrec  42775
  Copyright terms: Public domain W3C validator