Theorem eqimss 4040

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  eqimss2  4041  sspss  4099  uneqin  4278  difn0  4364  ssdisj  4459  uneqdifeq  4492  pweq  4616  pwpw0  4816  ssprsseq  4828  sssn  4829  snsspw  4845  pwsnOLD  4901  unieq  4919  unissint  4976  pwpwssunieq  5107  elpwuni  5108  disjeq2  5117  disjeq1  5120  pwne  5350  pwssun  5571  poeq2  5592  freq2  5647  seeq1  5648  seeq2  5649  frsn  5763  dmxpss  6170  xp11  6174  dmsnopss  6213  trsucss  6452  suc11  6471  iotassuni  6515  iotassuniOLD  6522  funeq  6568  fnresdm  6669  fssxp  6745  ffdm  6747  fcoi1  6765  fof  6805  dff1o2  6838  fvmptss  7010  fvmptss2  7023  funressn  7159  dff1o6  7275  sucexeloniOLD  7800  suceloniOLD  7802  tposeq  8215  tfrlem11  8390  oewordi  8593  oewordri  8594  dffi3  9428  cantnfle  9668  cantnflem2  9687  r1ord3g  9776  rankeq0b  9857  rankxplim3  9878  carddom2  9974  cflm  10247  cfsuc  10254  isf32lem2  10351  axdc3lem2  10448  ttukeylem5  10510  tsksuc  10759  fsuppmapnn0fiublem  13959  fsuppmapnn0fiub  13960  xptrrel  14931  relexpnndm  14992  relexpdmg  14993  relexprng  14997  relexpfld  15000  relexpaddg  15004  invf  17719  sscres  17774  pgpssslw  19523  fislw  19534  frgpup1  19684  frgpup3lem  19686  dprdspan  19938  dprdz  19941  dprdf1o  19943  dprd2da  19953  ablfac1b  19981  lspsncmp  20874  lspsnne2  20876  lspsneq  20880  psgnghm2  21353  psrbaglesupp  21696  psrbaglesuppOLD  21697  psrbaglefi  21704  psrbaglefiOLD  21705  mplcoe5  21814  mplbas2  21816  ofco2  22173  toprntopon  22647  cncnpi  23002  hauscmplem  23130  iskgen2  23272  elqtop3  23427  qtoprest  23441  hmeores  23495  snfil  23588  uffixfr  23647  ustuqtop2  23967  tngngp2  24389  metnrmlem3  24597  volcn  25347  recnprss  25645  plyeq0  25949  madebdaylemlrcut  27618  uhgr3cyclex  29690  chsupsn  30921  chlejb1i  30984  atsseq  31855  disjeq1f  32059  ldgenpisys  33450  measxun2  33494  measssd  33499  measiuns  33501  pmeasmono  33609  eulerpartlemb  33653  bnj1143  34087  bnj1322  34119  funsseq  35031  opnbnd  35513  cldbnd  35514  fnemeet1  35554  bj-restuni  36281  bj-inexeqex  36338  bj-idreseq  36346  relowlpssretop  36548  pibt2  36601  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  heiborlem10  36991  smprngopr  37223  funALTVeq  37873  disjeq  37907  lshpcmp  38161  lsatcmp  38176  lsatcmp2  38177  lshpset2N  38292  paddasslem17  39010  pcl0bN  39097  pexmidALTN  39152  lcfrlem26  40742  lcfrlem36  40752  mapd0  40839  nacsfix  41752  minregex  42587  cbviuneq12df  42714  relexp0a  42769  relexpaddss  42771  frege124d  42814  k0004lem3  43202  dvconstbi  43395  ssin0  44044  icccncfext  44902  dvmptconst  44930  dvmptidg  44932  dvmulcncf  44940  dvdivcncf  44942  dirkercncflem2  45119  fourierdlem70  45191  fourierdlem71  45192  hoicvr  45563  ovnsubaddlem1  45585  ovnhoi  45618  hspdifhsp  45631  fcoreslem4  46075  seppsepf  47649  intubeu  47697  setrec2mpt  47830  0setrec  47837