Theorem eqimss 3992

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

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

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 2708

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

This theorem is referenced by:  eqimss2  3993  sspss  4054  uneqin  4241  difn0  4319  ssdisj  4412  uneqdifeq  4445  pweq  4568  pwpw0  4769  ssprsseq  4781  sssn  4782  snsspw  4800  unieq  4874  unissint  4927  pwpwssunieq  5059  elpwuni  5060  disjeq2  5069  disjeq1  5072  pwne  5298  pwssun  5516  poeq2  5536  freq2  5592  seeq1  5594  seeq2  5595  frsn  5712  dmxpss  6129  xp11  6133  dmsnopss  6172  trsucss  6407  suc11  6426  iotassuni  6467  funeq  6512  fnresdm  6611  fssxp  6689  ffdm  6691  fcoi1  6708  fof  6746  dff1o2  6779  fvmptss  6953  fvmptss2  6967  funressn  7104  dff1o6  7221  tposeq  8170  tfrlem11  8319  oewordi  8519  oewordri  8520  dffi3  9334  cantnfle  9580  cantnflem2  9599  r1ord3g  9691  rankeq0b  9772  rankxplim3  9793  carddom2  9889  cflm  10160  cfsuc  10167  isf32lem2  10264  axdc3lem2  10361  ttukeylem5  10423  tsksuc  10673  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  xptrrel  14903  relexpnndm  14964  relexpdmg  14965  relexprng  14969  relexpfld  14972  relexpaddg  14976  invf  17692  sscres  17747  pgpssslw  19543  fislw  19554  frgpup1  19704  frgpup3lem  19706  dprdspan  19958  dprdz  19961  dprdf1o  19963  dprd2da  19973  ablfac1b  20001  lspsncmp  21071  lspsnne2  21073  lspsneq  21077  psgnghm2  21536  psrbaglesupp  21878  psrbaglefi  21882  mplcoe5  21995  mplbas2  21997  ofco2  22395  toprntopon  22869  cncnpi  23222  hauscmplem  23350  iskgen2  23492  elqtop3  23647  qtoprest  23661  hmeores  23715  snfil  23808  uffixfr  23867  ustuqtop2  24186  tngngp2  24596  metnrmlem3  24806  volcn  25563  recnprss  25861  plyeq0  26172  madebdaylemlrcut  27895  uhgr3cyclex  30257  chsupsn  31488  chlejb1i  31551  atsseq  32422  disjeq1f  32648  ldgenpisys  34323  measxun2  34367  measssd  34372  measiuns  34374  pmeasmono  34481  eulerpartlemb  34525  bnj1143  34946  bnj1322  34978  funsseq  35962  opnbnd  36519  cldbnd  36520  fnemeet1  36560  bj-restuni  37302  bj-inexeqex  37359  bj-idreseq  37367  relowlpssretop  37569  pibt2  37622  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  heiborlem10  38021  smprngopr  38253  funALTVeq  38959  disjeq  38993  lshpcmp  39248  lsatcmp  39263  lsatcmp2  39264  lshpset2N  39379  paddasslem17  40096  pcl0bN  40183  pexmidALTN  40238  lcfrlem26  41828  lcfrlem36  41838  mapd0  41925  nacsfix  42954  minregex  43775  cbviuneq12df  43902  relexp0a  43957  relexpaddss  43959  frege124d  44002  k0004lem3  44390  dvconstbi  44575  ssin0  45300  icccncfext  46131  dvmptconst  46159  dvmptidg  46161  dvmulcncf  46169  dvdivcncf  46171  dirkercncflem2  46348  fourierdlem70  46420  fourierdlem71  46421  hoicvr  46792  ovnsubaddlem1  46814  ovnhoi  46847  hspdifhsp  46860  fcoreslem4  47312  iuneqconst2  49068  iineqconst2  49069  seppsepf  49174  intubeu  49229  setrec2mpt  49942  0setrec  49949