Theorem eqimss 4038

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  eqimss2  4039  sspss  4097  uneqin  4279  difn0  4366  ssdisj  4461  uneqdifeq  4494  pweq  4618  pwpw0  4819  ssprsseq  4831  sssn  4832  snsspw  4848  unieq  4921  unissint  4977  pwpwssunieq  5109  elpwuni  5110  disjeq2  5119  disjeq1  5122  pwne  5354  pwssun  5575  poeq2  5596  freq2  5651  seeq1  5652  seeq2  5653  frsn  5767  dmxpss  6178  xp11  6182  dmsnopss  6221  trsucss  6460  suc11  6479  iotassuni  6523  iotassuniOLD  6530  funeq  6576  fnresdm  6677  fssxp  6754  ffdm  6756  fcoi1  6774  fof  6814  dff1o2  6847  fvmptss  7020  fvmptss2  7034  funressn  7172  dff1o6  7288  sucexeloniOLD  7817  suceloniOLD  7819  tposeq  8238  tfrlem11  8413  oewordi  8616  oewordri  8617  dffi3  9460  cantnfle  9700  cantnflem2  9719  r1ord3g  9808  rankeq0b  9889  rankxplim3  9910  carddom2  10006  cflm  10279  cfsuc  10286  isf32lem2  10383  axdc3lem2  10480  ttukeylem5  10542  tsksuc  10791  fsuppmapnn0fiublem  13993  fsuppmapnn0fiub  13994  xptrrel  14965  relexpnndm  15026  relexpdmg  15027  relexprng  15031  relexpfld  15034  relexpaddg  15038  invf  17756  sscres  17811  pgpssslw  19574  fislw  19585  frgpup1  19735  frgpup3lem  19737  dprdspan  19989  dprdz  19992  dprdf1o  19994  dprd2da  20004  ablfac1b  20032  lspsncmp  21009  lspsnne2  21011  lspsneq  21015  psgnghm2  21518  psrbaglesupp  21862  psrbaglesuppOLD  21863  psrbaglefi  21870  psrbaglefiOLD  21871  mplcoe5  21983  mplbas2  21985  ofco2  22371  toprntopon  22845  cncnpi  23200  hauscmplem  23328  iskgen2  23470  elqtop3  23625  qtoprest  23639  hmeores  23693  snfil  23786  uffixfr  23845  ustuqtop2  24165  tngngp2  24587  metnrmlem3  24795  volcn  25553  recnprss  25851  plyeq0  26163  madebdaylemlrcut  27843  uhgr3cyclex  30010  chsupsn  31241  chlejb1i  31304  atsseq  32175  disjeq1f  32381  ldgenpisys  33790  measxun2  33834  measssd  33839  measiuns  33841  pmeasmono  33949  eulerpartlemb  33993  bnj1143  34426  bnj1322  34458  funsseq  35368  opnbnd  35814  cldbnd  35815  fnemeet1  35855  bj-restuni  36581  bj-inexeqex  36638  bj-idreseq  36646  relowlpssretop  36848  pibt2  36901  ovoliunnfl  37140  voliunnfl  37142  volsupnfl  37143  heiborlem10  37298  smprngopr  37530  funALTVeq  38176  disjeq  38210  lshpcmp  38464  lsatcmp  38479  lsatcmp2  38480  lshpset2N  38595  paddasslem17  39313  pcl0bN  39400  pexmidALTN  39455  lcfrlem26  41045  lcfrlem36  41055  mapd0  41142  nacsfix  42135  minregex  42967  cbviuneq12df  43094  relexp0a  43149  relexpaddss  43151  frege124d  43194  k0004lem3  43582  dvconstbi  43774  ssin0  44422  icccncfext  45277  dvmptconst  45305  dvmptidg  45307  dvmulcncf  45315  dvdivcncf  45317  dirkercncflem2  45494  fourierdlem70  45566  fourierdlem71  45567  hoicvr  45938  ovnsubaddlem1  45960  ovnhoi  45993  hspdifhsp  46006  fcoreslem4  46450  seppsepf  47998  intubeu  48046  setrec2mpt  48179  0setrec  48186