Theorem eqimss 4002

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqimss2  4003  sspss  4061  uneqin  4248  difn0  4326  ssdisj  4419  uneqdifeq  4452  pweq  4573  pwpw0  4773  ssprsseq  4785  sssn  4786  snsspw  4804  unieq  4878  unissint  4932  pwpwssunieq  5063  elpwuni  5064  disjeq2  5073  disjeq1  5076  pwne  5303  pwssun  5523  poeq2  5543  freq2  5599  seeq1  5601  seeq2  5602  frsn  5719  dmxpss  6132  xp11  6136  dmsnopss  6175  trsucss  6410  suc11  6429  iotassuni  6471  iotassuniOLD  6478  funeq  6520  fnresdm  6619  fssxp  6697  ffdm  6699  fcoi1  6716  fof  6754  dff1o2  6787  fvmptss  6962  fvmptss2  6976  funressn  7113  dff1o6  7232  sucexeloniOLD  7766  tposeq  8184  tfrlem11  8333  oewordi  8532  oewordri  8533  dffi3  9358  cantnfle  9600  cantnflem2  9619  r1ord3g  9708  rankeq0b  9789  rankxplim3  9810  carddom2  9906  cflm  10179  cfsuc  10186  isf32lem2  10283  axdc3lem2  10380  ttukeylem5  10442  tsksuc  10691  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  xptrrel  14922  relexpnndm  14983  relexpdmg  14984  relexprng  14988  relexpfld  14991  relexpaddg  14995  invf  17706  sscres  17761  pgpssslw  19520  fislw  19531  frgpup1  19681  frgpup3lem  19683  dprdspan  19935  dprdz  19938  dprdf1o  19940  dprd2da  19950  ablfac1b  19978  lspsncmp  21002  lspsnne2  21004  lspsneq  21008  psgnghm2  21466  psrbaglesupp  21807  psrbaglefi  21811  mplcoe5  21923  mplbas2  21925  ofco2  22314  toprntopon  22788  cncnpi  23141  hauscmplem  23269  iskgen2  23411  elqtop3  23566  qtoprest  23580  hmeores  23634  snfil  23727  uffixfr  23786  ustuqtop2  24106  tngngp2  24516  metnrmlem3  24726  volcn  25483  recnprss  25781  plyeq0  26092  madebdaylemlrcut  27786  uhgr3cyclex  30084  chsupsn  31315  chlejb1i  31378  atsseq  32249  disjeq1f  32475  ldgenpisys  34129  measxun2  34173  measssd  34178  measiuns  34180  pmeasmono  34288  eulerpartlemb  34332  bnj1143  34753  bnj1322  34785  funsseq  35728  opnbnd  36286  cldbnd  36287  fnemeet1  36327  bj-restuni  37058  bj-inexeqex  37115  bj-idreseq  37123  relowlpssretop  37325  pibt2  37378  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  heiborlem10  37787  smprngopr  38019  funALTVeq  38665  disjeq  38699  lshpcmp  38954  lsatcmp  38969  lsatcmp2  38970  lshpset2N  39085  paddasslem17  39803  pcl0bN  39890  pexmidALTN  39945  lcfrlem26  41535  lcfrlem36  41545  mapd0  41632  nacsfix  42673  minregex  43496  cbviuneq12df  43623  relexp0a  43678  relexpaddss  43680  frege124d  43723  k0004lem3  44111  dvconstbi  44296  ssin0  45022  icccncfext  45858  dvmptconst  45886  dvmptidg  45888  dvmulcncf  45896  dvdivcncf  45898  dirkercncflem2  46075  fourierdlem70  46147  fourierdlem71  46148  hoicvr  46519  ovnsubaddlem1  46541  ovnhoi  46574  hspdifhsp  46587  fcoreslem4  47040  iuneqconst2  48784  iineqconst2  48785  seppsepf  48890  intubeu  48945  setrec2mpt  49659  0setrec  49666