Theorem eqimss 3990

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

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

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 2123  ax-ext 2706

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

This theorem is referenced by:  eqimss2  3991  sspss  4052  uneqin  4239  difn0  4317  ssdisj  4410  uneqdifeq  4443  pweq  4566  pwpw0  4767  ssprsseq  4779  sssn  4780  snsspw  4798  unieq  4872  unissint  4925  pwpwssunieq  5057  elpwuni  5058  disjeq2  5067  disjeq1  5070  pwne  5296  pwssun  5514  poeq2  5534  freq2  5590  seeq1  5592  seeq2  5593  frsn  5710  dmxpss  6127  xp11  6131  dmsnopss  6170  trsucss  6405  suc11  6424  iotassuni  6465  funeq  6510  fnresdm  6609  fssxp  6687  ffdm  6689  fcoi1  6706  fof  6744  dff1o2  6777  fvmptss  6951  fvmptss2  6965  funressn  7102  dff1o6  7219  tposeq  8168  tfrlem11  8317  oewordi  8517  oewordri  8518  dffi3  9332  cantnfle  9578  cantnflem2  9597  r1ord3g  9689  rankeq0b  9770  rankxplim3  9791  carddom2  9887  cflm  10158  cfsuc  10165  isf32lem2  10262  axdc3lem2  10359  ttukeylem5  10421  tsksuc  10671  fsuppmapnn0fiublem  13911  fsuppmapnn0fiub  13912  xptrrel  14901  relexpnndm  14962  relexpdmg  14963  relexprng  14967  relexpfld  14970  relexpaddg  14974  invf  17690  sscres  17745  pgpssslw  19541  fislw  19552  frgpup1  19702  frgpup3lem  19704  dprdspan  19956  dprdz  19959  dprdf1o  19961  dprd2da  19971  ablfac1b  19999  lspsncmp  21069  lspsnne2  21071  lspsneq  21075  psgnghm2  21534  psrbaglesupp  21876  psrbaglefi  21880  mplcoe5  21993  mplbas2  21995  ofco2  22393  toprntopon  22867  cncnpi  23220  hauscmplem  23348  iskgen2  23490  elqtop3  23645  qtoprest  23659  hmeores  23713  snfil  23806  uffixfr  23865  ustuqtop2  24184  tngngp2  24594  metnrmlem3  24804  volcn  25561  recnprss  25859  plyeq0  26170  madebdaylemlrcut  27871  uhgr3cyclex  30206  chsupsn  31437  chlejb1i  31500  atsseq  32371  disjeq1f  32597  ldgenpisys  34272  measxun2  34316  measssd  34321  measiuns  34323  pmeasmono  34430  eulerpartlemb  34474  bnj1143  34895  bnj1322  34927  funsseq  35911  opnbnd  36468  cldbnd  36469  fnemeet1  36509  bj-restuni  37241  bj-inexeqex  37298  bj-idreseq  37306  relowlpssretop  37508  pibt2  37561  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  heiborlem10  37960  smprngopr  38192  funALTVeq  38898  disjeq  38932  lshpcmp  39187  lsatcmp  39202  lsatcmp2  39203  lshpset2N  39318  paddasslem17  40035  pcl0bN  40122  pexmidALTN  40177  lcfrlem26  41767  lcfrlem36  41777  mapd0  41864  nacsfix  42896  minregex  43717  cbviuneq12df  43844  relexp0a  43899  relexpaddss  43901  frege124d  43944  k0004lem3  44332  dvconstbi  44517  ssin0  45242  icccncfext  46073  dvmptconst  46101  dvmptidg  46103  dvmulcncf  46111  dvdivcncf  46113  dirkercncflem2  46290  fourierdlem70  46362  fourierdlem71  46363  hoicvr  46734  ovnsubaddlem1  46756  ovnhoi  46789  hspdifhsp  46802  fcoreslem4  47254  iuneqconst2  49010  iineqconst2  49011  seppsepf  49116  intubeu  49171  setrec2mpt  49884  0setrec  49891