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  17710  sscres  17765  pgpssslw  19528  fislw  19539  frgpup1  19689  frgpup3lem  19691  dprdspan  19943  dprdz  19946  dprdf1o  19948  dprd2da  19958  ablfac1b  19986  lspsncmp  21058  lspsnne2  21060  lspsneq  21064  psgnghm2  21523  psrbaglesupp  21864  psrbaglefi  21868  mplcoe5  21980  mplbas2  21982  ofco2  22371  toprntopon  22845  cncnpi  23198  hauscmplem  23326  iskgen2  23468  elqtop3  23623  qtoprest  23637  hmeores  23691  snfil  23784  uffixfr  23843  ustuqtop2  24163  tngngp2  24573  metnrmlem3  24783  volcn  25540  recnprss  25838  plyeq0  26149  madebdaylemlrcut  27848  uhgr3cyclex  30161  chsupsn  31392  chlejb1i  31455  atsseq  32326  disjeq1f  32552  ldgenpisys  34149  measxun2  34193  measssd  34198  measiuns  34200  pmeasmono  34308  eulerpartlemb  34352  bnj1143  34773  bnj1322  34805  funsseq  35748  opnbnd  36306  cldbnd  36307  fnemeet1  36347  bj-restuni  37078  bj-inexeqex  37135  bj-idreseq  37143  relowlpssretop  37345  pibt2  37398  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  heiborlem10  37807  smprngopr  38039  funALTVeq  38685  disjeq  38719  lshpcmp  38974  lsatcmp  38989  lsatcmp2  38990  lshpset2N  39105  paddasslem17  39823  pcl0bN  39910  pexmidALTN  39965  lcfrlem26  41555  lcfrlem36  41565  mapd0  41652  nacsfix  42693  minregex  43516  cbviuneq12df  43643  relexp0a  43698  relexpaddss  43700  frege124d  43743  k0004lem3  44131  dvconstbi  44316  ssin0  45042  icccncfext  45878  dvmptconst  45906  dvmptidg  45908  dvmulcncf  45916  dvdivcncf  45918  dirkercncflem2  46095  fourierdlem70  46167  fourierdlem71  46168  hoicvr  46539  ovnsubaddlem1  46561  ovnhoi  46594  hspdifhsp  46607  fcoreslem4  47060  iuneqconst2  48804  iineqconst2  48805  seppsepf  48910  intubeu  48965  setrec2mpt  49679  0setrec  49686