Theorem eqimss 3988

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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqimssd 3986	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  eqimss2  3989  sspss  4049  uneqin  4236  difn0  4314  ssdisj  4407  uneqdifeq  4440  pweq  4561  pwpw0  4762  ssprsseq  4774  sssn  4775  snsspw  4793  unieq  4867  unissint  4920  pwpwssunieq  5050  elpwuni  5051  disjeq2  5060  disjeq1  5063  pwne  5289  pwssun  5506  poeq2  5526  freq2  5582  seeq1  5584  seeq2  5585  frsn  5702  dmxpss  6118  xp11  6122  dmsnopss  6161  trsucss  6396  suc11  6415  iotassuni  6456  funeq  6501  fnresdm  6600  fssxp  6678  ffdm  6680  fcoi1  6697  fof  6735  dff1o2  6768  fvmptss  6941  fvmptss2  6955  funressn  7092  dff1o6  7209  tposeq  8158  tfrlem11  8307  oewordi  8506  oewordri  8507  dffi3  9315  cantnfle  9561  cantnflem2  9580  r1ord3g  9672  rankeq0b  9753  rankxplim3  9774  carddom2  9870  cflm  10141  cfsuc  10148  isf32lem2  10245  axdc3lem2  10342  ttukeylem5  10404  tsksuc  10653  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  xptrrel  14887  relexpnndm  14948  relexpdmg  14949  relexprng  14953  relexpfld  14956  relexpaddg  14960  invf  17675  sscres  17730  pgpssslw  19526  fislw  19537  frgpup1  19687  frgpup3lem  19689  dprdspan  19941  dprdz  19944  dprdf1o  19946  dprd2da  19956  ablfac1b  19984  lspsncmp  21053  lspsnne2  21055  lspsneq  21059  psgnghm2  21518  psrbaglesupp  21859  psrbaglefi  21863  mplcoe5  21975  mplbas2  21977  ofco2  22366  toprntopon  22840  cncnpi  23193  hauscmplem  23321  iskgen2  23463  elqtop3  23618  qtoprest  23632  hmeores  23686  snfil  23779  uffixfr  23838  ustuqtop2  24157  tngngp2  24567  metnrmlem3  24777  volcn  25534  recnprss  25832  plyeq0  26143  madebdaylemlrcut  27844  uhgr3cyclex  30162  chsupsn  31393  chlejb1i  31456  atsseq  32327  disjeq1f  32553  ldgenpisys  34179  measxun2  34223  measssd  34228  measiuns  34230  pmeasmono  34337  eulerpartlemb  34381  bnj1143  34802  bnj1322  34834  funsseq  35812  opnbnd  36367  cldbnd  36368  fnemeet1  36408  bj-restuni  37139  bj-inexeqex  37196  bj-idreseq  37204  relowlpssretop  37406  pibt2  37459  ovoliunnfl  37710  voliunnfl  37712  volsupnfl  37713  heiborlem10  37868  smprngopr  38100  funALTVeq  38746  disjeq  38780  lshpcmp  39035  lsatcmp  39050  lsatcmp2  39051  lshpset2N  39166  paddasslem17  39883  pcl0bN  39970  pexmidALTN  40025  lcfrlem26  41615  lcfrlem36  41625  mapd0  41712  nacsfix  42753  minregex  43575  cbviuneq12df  43702  relexp0a  43757  relexpaddss  43759  frege124d  43802  k0004lem3  44190  dvconstbi  44375  ssin0  45100  icccncfext  45933  dvmptconst  45961  dvmptidg  45963  dvmulcncf  45971  dvdivcncf  45973  dirkercncflem2  46150  fourierdlem70  46222  fourierdlem71  46223  hoicvr  46594  ovnsubaddlem1  46616  ovnhoi  46649  hspdifhsp  46662  fcoreslem4  47105  iuneqconst2  48862  iineqconst2  48863  seppsepf  48968  intubeu  49023  setrec2mpt  49737  0setrec  49744