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

Theorem eqimss 3998
Description: Equality implies inclusion. (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 3957 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 498 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wss 3908
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-in 3915  df-ss 3925
This theorem is referenced by:  eqimss2  3999  sspss  4057  uneqin  4236  difn0  4322  ssdisj  4417  uneqdifeq  4448  pweq  4572  pwpw0  4771  ssprsseq  4783  sssn  4784  snsspw  4800  pwsnOLD  4856  unieq  4874  unissint  4931  pwpwssunieq  5062  elpwuni  5063  disjeq2  5072  disjeq1  5075  pwne  5305  pwssun  5526  poeq2  5547  freq2  5602  seeq1  5603  seeq2  5604  frsn  5717  dmxpss  6121  xp11  6125  dmsnopss  6164  trsucss  6403  suc11  6421  iotassuni  6465  iotassuniOLD  6472  funeq  6518  fnresdm  6617  fssxp  6693  ffdm  6695  fcoi1  6713  fof  6753  dff1o2  6786  fvmptss  6957  fvmptss2  6970  funressn  7101  dff1o6  7217  sucexeloniOLD  7741  suceloniOLD  7743  tposeq  8155  tfrlem11  8330  oewordi  8534  oewordri  8535  dffi3  9363  cantnfle  9603  cantnflem2  9622  r1ord3g  9711  rankeq0b  9792  rankxplim3  9813  carddom2  9909  cflm  10182  cfsuc  10189  isf32lem2  10286  axdc3lem2  10383  ttukeylem5  10445  tsksuc  10694  fsuppmapnn0fiublem  13887  fsuppmapnn0fiub  13888  xptrrel  14857  relexpnndm  14918  relexpdmg  14919  relexprng  14923  relexpfld  14926  relexpaddg  14930  invf  17643  sscres  17698  pgpssslw  19387  fislw  19398  frgpup1  19548  frgpup3lem  19550  dprdspan  19797  dprdz  19800  dprdf1o  19802  dprd2da  19812  ablfac1b  19840  lspsncmp  20562  lspsnne2  20564  lspsneq  20568  psgnghm2  20970  psrbaglesupp  21311  psrbaglesuppOLD  21312  psrbaglefi  21319  psrbaglefiOLD  21320  mplcoe5  21425  mplbas2  21427  ofco2  21784  toprntopon  22258  cncnpi  22613  hauscmplem  22741  iskgen2  22883  elqtop3  23038  qtoprest  23052  hmeores  23106  snfil  23199  uffixfr  23258  ustuqtop2  23578  tngngp2  24000  metnrmlem3  24208  volcn  24954  recnprss  25252  plyeq0  25556  madebdaylemlrcut  27212  uhgr3cyclex  29012  chsupsn  30241  chlejb1i  30304  atsseq  31175  disjeq1f  31377  ldgenpisys  32634  measxun2  32678  measssd  32683  measiuns  32685  pmeasmono  32793  eulerpartlemb  32837  bnj1143  33271  bnj1322  33303  funsseq  34212  opnbnd  34764  cldbnd  34765  fnemeet1  34805  bj-restuni  35535  bj-inexeqex  35592  bj-idreseq  35600  relowlpssretop  35802  pibt2  35855  ovoliunnfl  36087  voliunnfl  36089  volsupnfl  36090  heiborlem10  36246  smprngopr  36478  funALTVeq  37129  disjeq  37163  lshpcmp  37417  lsatcmp  37432  lsatcmp2  37433  lshpset2N  37548  paddasslem17  38266  pcl0bN  38353  pexmidALTN  38408  lcfrlem26  39998  lcfrlem36  40008  mapd0  40095  nacsfix  40973  minregex  41748  cbviuneq12df  41875  relexp0a  41930  relexpaddss  41932  frege124d  41975  k0004lem3  42363  dvconstbi  42556  ssin0  43205  icccncfext  44060  dvmptconst  44088  dvmptidg  44090  dvmulcncf  44098  dvdivcncf  44100  dirkercncflem2  44277  fourierdlem70  44349  fourierdlem71  44350  hoicvr  44721  ovnsubaddlem1  44743  ovnhoi  44776  hspdifhsp  44789  fcoreslem4  45232  seppsepf  46893  intubeu  46941  setrec2mpt  47074  0setrec  47081
  Copyright terms: Public domain W3C validator