Theorem eqimss 4017

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqimss2  4018  sspss  4077  uneqin  4264  difn0  4342  ssdisj  4435  uneqdifeq  4468  pweq  4589  pwpw0  4789  ssprsseq  4801  sssn  4802  snsspw  4820  unieq  4894  unissint  4948  pwpwssunieq  5080  elpwuni  5081  disjeq2  5090  disjeq1  5093  pwne  5323  pwssun  5545  poeq2  5565  freq2  5622  seeq1  5624  seeq2  5625  frsn  5742  dmxpss  6160  xp11  6164  dmsnopss  6203  trsucss  6442  suc11  6461  iotassuni  6503  iotassuniOLD  6510  funeq  6556  fnresdm  6657  fssxp  6733  ffdm  6735  fcoi1  6752  fof  6790  dff1o2  6823  fvmptss  6998  fvmptss2  7012  funressn  7149  dff1o6  7268  sucexeloniOLD  7804  suceloniOLD  7806  tposeq  8227  tfrlem11  8402  oewordi  8603  oewordri  8604  dffi3  9443  cantnfle  9685  cantnflem2  9704  r1ord3g  9793  rankeq0b  9874  rankxplim3  9895  carddom2  9991  cflm  10264  cfsuc  10271  isf32lem2  10368  axdc3lem2  10465  ttukeylem5  10527  tsksuc  10776  fsuppmapnn0fiublem  14008  fsuppmapnn0fiub  14009  xptrrel  14999  relexpnndm  15060  relexpdmg  15061  relexprng  15065  relexpfld  15068  relexpaddg  15072  invf  17781  sscres  17836  pgpssslw  19595  fislw  19606  frgpup1  19756  frgpup3lem  19758  dprdspan  20010  dprdz  20013  dprdf1o  20015  dprd2da  20025  ablfac1b  20053  lspsncmp  21077  lspsnne2  21079  lspsneq  21083  psgnghm2  21541  psrbaglesupp  21882  psrbaglefi  21886  mplcoe5  21998  mplbas2  22000  ofco2  22389  toprntopon  22863  cncnpi  23216  hauscmplem  23344  iskgen2  23486  elqtop3  23641  qtoprest  23655  hmeores  23709  snfil  23802  uffixfr  23861  ustuqtop2  24181  tngngp2  24591  metnrmlem3  24801  volcn  25559  recnprss  25857  plyeq0  26168  madebdaylemlrcut  27862  uhgr3cyclex  30163  chsupsn  31394  chlejb1i  31457  atsseq  32328  disjeq1f  32554  ldgenpisys  34197  measxun2  34241  measssd  34246  measiuns  34248  pmeasmono  34356  eulerpartlemb  34400  bnj1143  34821  bnj1322  34853  funsseq  35785  opnbnd  36343  cldbnd  36344  fnemeet1  36384  bj-restuni  37115  bj-inexeqex  37172  bj-idreseq  37180  relowlpssretop  37382  pibt2  37435  ovoliunnfl  37686  voliunnfl  37688  volsupnfl  37689  heiborlem10  37844  smprngopr  38076  funALTVeq  38718  disjeq  38752  lshpcmp  39006  lsatcmp  39021  lsatcmp2  39022  lshpset2N  39137  paddasslem17  39855  pcl0bN  39942  pexmidALTN  39997  lcfrlem26  41587  lcfrlem36  41597  mapd0  41684  nacsfix  42735  minregex  43558  cbviuneq12df  43685  relexp0a  43740  relexpaddss  43742  frege124d  43785  k0004lem3  44173  dvconstbi  44358  ssin0  45079  icccncfext  45916  dvmptconst  45944  dvmptidg  45946  dvmulcncf  45954  dvdivcncf  45956  dirkercncflem2  46133  fourierdlem70  46205  fourierdlem71  46206  hoicvr  46577  ovnsubaddlem1  46599  ovnhoi  46632  hspdifhsp  46645  fcoreslem4  47095  iuneqconst2  48801  iineqconst2  48802  seppsepf  48903  intubeu  48958  setrec2mpt  49561  0setrec  49568