Theorem eqimss 4008

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  eqimss2  4009  sspss  4068  uneqin  4255  difn0  4333  ssdisj  4426  uneqdifeq  4459  pweq  4580  pwpw0  4780  ssprsseq  4792  sssn  4793  snsspw  4811  unieq  4885  unissint  4939  pwpwssunieq  5071  elpwuni  5072  disjeq2  5081  disjeq1  5084  pwne  5311  pwssun  5533  poeq2  5553  freq2  5609  seeq1  5611  seeq2  5612  frsn  5729  dmxpss  6147  xp11  6151  dmsnopss  6190  trsucss  6425  suc11  6444  iotassuni  6486  iotassuniOLD  6493  funeq  6539  fnresdm  6640  fssxp  6718  ffdm  6720  fcoi1  6737  fof  6775  dff1o2  6808  fvmptss  6983  fvmptss2  6997  funressn  7134  dff1o6  7253  sucexeloniOLD  7789  tposeq  8210  tfrlem11  8359  oewordi  8558  oewordri  8559  dffi3  9389  cantnfle  9631  cantnflem2  9650  r1ord3g  9739  rankeq0b  9820  rankxplim3  9841  carddom2  9937  cflm  10210  cfsuc  10217  isf32lem2  10314  axdc3lem2  10411  ttukeylem5  10473  tsksuc  10722  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  xptrrel  14953  relexpnndm  15014  relexpdmg  15015  relexprng  15019  relexpfld  15022  relexpaddg  15026  invf  17737  sscres  17792  pgpssslw  19551  fislw  19562  frgpup1  19712  frgpup3lem  19714  dprdspan  19966  dprdz  19969  dprdf1o  19971  dprd2da  19981  ablfac1b  20009  lspsncmp  21033  lspsnne2  21035  lspsneq  21039  psgnghm2  21497  psrbaglesupp  21838  psrbaglefi  21842  mplcoe5  21954  mplbas2  21956  ofco2  22345  toprntopon  22819  cncnpi  23172  hauscmplem  23300  iskgen2  23442  elqtop3  23597  qtoprest  23611  hmeores  23665  snfil  23758  uffixfr  23817  ustuqtop2  24137  tngngp2  24547  metnrmlem3  24757  volcn  25514  recnprss  25812  plyeq0  26123  madebdaylemlrcut  27817  uhgr3cyclex  30118  chsupsn  31349  chlejb1i  31412  atsseq  32283  disjeq1f  32509  ldgenpisys  34163  measxun2  34207  measssd  34212  measiuns  34214  pmeasmono  34322  eulerpartlemb  34366  bnj1143  34787  bnj1322  34819  funsseq  35762  opnbnd  36320  cldbnd  36321  fnemeet1  36361  bj-restuni  37092  bj-inexeqex  37149  bj-idreseq  37157  relowlpssretop  37359  pibt2  37412  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  heiborlem10  37821  smprngopr  38053  funALTVeq  38699  disjeq  38733  lshpcmp  38988  lsatcmp  39003  lsatcmp2  39004  lshpset2N  39119  paddasslem17  39837  pcl0bN  39924  pexmidALTN  39979  lcfrlem26  41569  lcfrlem36  41579  mapd0  41666  nacsfix  42707  minregex  43530  cbviuneq12df  43657  relexp0a  43712  relexpaddss  43714  frege124d  43757  k0004lem3  44145  dvconstbi  44330  ssin0  45056  icccncfext  45892  dvmptconst  45920  dvmptidg  45922  dvmulcncf  45930  dvdivcncf  45932  dirkercncflem2  46109  fourierdlem70  46181  fourierdlem71  46182  hoicvr  46553  ovnsubaddlem1  46575  ovnhoi  46608  hspdifhsp  46621  fcoreslem4  47071  iuneqconst2  48815  iineqconst2  48816  seppsepf  48921  intubeu  48976  setrec2mpt  49690  0setrec  49697