Theorem eqimss 3994

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 3992	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqimss2  3995  sspss  4056  uneqin  4243  difn0  4321  ssdisj  4414  uneqdifeq  4447  pweq  4570  pwpw0  4771  ssprsseq  4783  sssn  4784  snsspw  4802  unieq  4876  unissint  4929  pwpwssunieq  5061  elpwuni  5062  disjeq2  5071  disjeq1  5074  pwne  5300  pwssun  5524  poeq2  5544  freq2  5600  seeq1  5602  seeq2  5603  frsn  5720  dmxpss  6137  xp11  6141  dmsnopss  6180  trsucss  6415  suc11  6434  iotassuni  6475  funeq  6520  fnresdm  6619  fssxp  6697  ffdm  6699  fcoi1  6716  fof  6754  dff1o2  6787  fvmptss  6962  fvmptss2  6976  funressn  7114  dff1o6  7231  tposeq  8180  tfrlem11  8329  oewordi  8529  oewordri  8530  dffi3  9346  cantnfle  9592  cantnflem2  9611  r1ord3g  9703  rankeq0b  9784  rankxplim3  9805  carddom2  9901  cflm  10172  cfsuc  10179  isf32lem2  10276  axdc3lem2  10373  ttukeylem5  10435  tsksuc  10685  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  xptrrel  14915  relexpnndm  14976  relexpdmg  14977  relexprng  14981  relexpfld  14984  relexpaddg  14988  invf  17704  sscres  17759  pgpssslw  19555  fislw  19566  frgpup1  19716  frgpup3lem  19718  dprdspan  19970  dprdz  19973  dprdf1o  19975  dprd2da  19985  ablfac1b  20013  lspsncmp  21083  lspsnne2  21085  lspsneq  21089  psgnghm2  21548  psrbaglesupp  21890  psrbaglefi  21894  mplcoe5  22007  mplbas2  22009  ofco2  22407  toprntopon  22881  cncnpi  23234  hauscmplem  23362  iskgen2  23504  elqtop3  23659  qtoprest  23673  hmeores  23727  snfil  23820  uffixfr  23879  ustuqtop2  24198  tngngp2  24608  metnrmlem3  24818  volcn  25575  recnprss  25873  plyeq0  26184  madebdaylemlrcut  27907  uhgr3cyclex  30269  chsupsn  31501  chlejb1i  31564  atsseq  32435  disjeq1f  32660  ldgenpisys  34344  measxun2  34388  measssd  34393  measiuns  34395  pmeasmono  34502  eulerpartlemb  34546  bnj1143  34966  bnj1322  34998  funsseq  35984  opnbnd  36541  cldbnd  36542  fnemeet1  36582  bj-restuni  37350  bj-inexeqex  37409  bj-idreseq  37417  relowlpssretop  37619  pibt2  37672  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  heiborlem10  38071  smprngopr  38303  funALTVeq  39036  disjeq  39085  lshpcmp  39364  lsatcmp  39379  lsatcmp2  39380  lshpset2N  39495  paddasslem17  40212  pcl0bN  40299  pexmidALTN  40354  lcfrlem26  41944  lcfrlem36  41954  mapd0  42041  nacsfix  43069  minregex  43890  cbviuneq12df  44017  relexp0a  44072  relexpaddss  44074  frege124d  44117  k0004lem3  44505  dvconstbi  44690  ssin0  45415  icccncfext  46245  dvmptconst  46273  dvmptidg  46275  dvmulcncf  46283  dvdivcncf  46285  dirkercncflem2  46462  fourierdlem70  46534  fourierdlem71  46535  hoicvr  46906  ovnsubaddlem1  46928  ovnhoi  46961  hspdifhsp  46974  fcoreslem4  47426  iuneqconst2  49182  iineqconst2  49183  seppsepf  49288  intubeu  49343  setrec2mpt  50056  0setrec  50063