Theorem eqimss 4041

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqimss2  4042  sspss  4100  uneqin  4279  difn0  4365  ssdisj  4460  uneqdifeq  4493  pweq  4617  pwpw0  4817  ssprsseq  4829  sssn  4830  snsspw  4846  pwsnOLD  4902  unieq  4920  unissint  4977  pwpwssunieq  5108  elpwuni  5109  disjeq2  5118  disjeq1  5121  pwne  5351  pwssun  5572  poeq2  5593  freq2  5648  seeq1  5649  seeq2  5650  frsn  5764  dmxpss  6171  xp11  6175  dmsnopss  6214  trsucss  6453  suc11  6472  iotassuni  6516  iotassuniOLD  6523  funeq  6569  fnresdm  6670  fssxp  6746  ffdm  6748  fcoi1  6766  fof  6806  dff1o2  6839  fvmptss  7011  fvmptss2  7024  funressn  7157  dff1o6  7273  sucexeloniOLD  7798  suceloniOLD  7800  tposeq  8213  tfrlem11  8388  oewordi  8591  oewordri  8592  dffi3  9426  cantnfle  9666  cantnflem2  9685  r1ord3g  9774  rankeq0b  9855  rankxplim3  9876  carddom2  9972  cflm  10245  cfsuc  10252  isf32lem2  10349  axdc3lem2  10446  ttukeylem5  10508  tsksuc  10757  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  xptrrel  14927  relexpnndm  14988  relexpdmg  14989  relexprng  14993  relexpfld  14996  relexpaddg  15000  invf  17715  sscres  17770  pgpssslw  19482  fislw  19493  frgpup1  19643  frgpup3lem  19645  dprdspan  19897  dprdz  19900  dprdf1o  19902  dprd2da  19912  ablfac1b  19940  lspsncmp  20729  lspsnne2  20731  lspsneq  20735  psgnghm2  21134  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrbaglefi  21485  psrbaglefiOLD  21486  mplcoe5  21595  mplbas2  21597  ofco2  21953  toprntopon  22427  cncnpi  22782  hauscmplem  22910  iskgen2  23052  elqtop3  23207  qtoprest  23221  hmeores  23275  snfil  23368  uffixfr  23427  ustuqtop2  23747  tngngp2  24169  metnrmlem3  24377  volcn  25123  recnprss  25421  plyeq0  25725  madebdaylemlrcut  27393  uhgr3cyclex  29435  chsupsn  30666  chlejb1i  30729  atsseq  31600  disjeq1f  31804  ldgenpisys  33164  measxun2  33208  measssd  33213  measiuns  33215  pmeasmono  33323  eulerpartlemb  33367  bnj1143  33801  bnj1322  33833  funsseq  34739  opnbnd  35210  cldbnd  35211  fnemeet1  35251  bj-restuni  35978  bj-inexeqex  36035  bj-idreseq  36043  relowlpssretop  36245  pibt2  36298  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  heiborlem10  36688  smprngopr  36920  funALTVeq  37570  disjeq  37604  lshpcmp  37858  lsatcmp  37873  lsatcmp2  37874  lshpset2N  37989  paddasslem17  38707  pcl0bN  38794  pexmidALTN  38849  lcfrlem26  40439  lcfrlem36  40449  mapd0  40536  nacsfix  41450  minregex  42285  cbviuneq12df  42412  relexp0a  42467  relexpaddss  42469  frege124d  42512  k0004lem3  42900  dvconstbi  43093  ssin0  43742  icccncfext  44603  dvmptconst  44631  dvmptidg  44633  dvmulcncf  44641  dvdivcncf  44643  dirkercncflem2  44820  fourierdlem70  44892  fourierdlem71  44893  hoicvr  45264  ovnsubaddlem1  45286  ovnhoi  45319  hspdifhsp  45332  fcoreslem4  45776  seppsepf  47561  intubeu  47609  setrec2mpt  47742  0setrec  47749