Theorem eqimss 3973

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqimss2  3974  sspss  4033  uneqin  4217  difn0  4295  ssdisj  4388  uneqdifeq  4420  pweq  4543  pwpw0  4744  ssprsseq  4756  sssn  4757  snsspw  4775  unieq  4849  unissint  4902  pwpwssunieq  5033  elpwuni  5034  disjeq2  5043  disjeq1  5046  pwne  5281  pwssun  5510  poeq2  5530  freq2  5586  seeq1  5588  seeq2  5589  frsn  5706  dmxpss  6122  xp11  6126  dmsnopss  6165  trsucss  6400  suc11  6419  iotassuni  6460  funeq  6505  fnresdm  6604  fssxp  6682  ffdm  6684  fcoi1  6701  fof  6739  dff1o2  6772  fvmptss  6948  fvmptss2  6962  funressn  7102  dff1o6  7219  tposeq  8168  tfrlem11  8317  oewordi  8517  oewordri  8518  dffi3  9334  cantnfle  9583  cantnflem2  9602  r1ord3g  9694  rankeq0b  9775  rankxplim3  9796  carddom2  9892  cflm  10163  cfsuc  10170  isf32lem2  10267  axdc3lem2  10364  ttukeylem5  10426  tsksuc  10676  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  xptrrel  14933  relexpnndm  14994  relexpdmg  14995  relexprng  14999  relexpfld  15002  relexpaddg  15006  invf  17726  sscres  17781  pgpssslw  19580  fislw  19591  frgpup1  19741  frgpup3lem  19743  dprdspan  19995  dprdz  19998  dprdf1o  20000  dprd2da  20010  ablfac1b  20038  lspsncmp  21109  lspsnne2  21111  lspsneq  21115  psgnghm2  21556  psrbaglesupp  21897  psrbaglefi  21901  mplcoe5  22016  mplbas2  22018  ofco2  22434  toprntopon  22908  cncnpi  23261  hauscmplem  23389  iskgen2  23531  elqtop3  23686  qtoprest  23700  hmeores  23754  snfil  23847  uffixfr  23906  ustuqtop2  24225  tngngp2  24635  metnrmlem3  24845  volcn  25591  recnprss  25889  plyeq0  26194  madebdaylemlrcut  27909  uhgr3cyclex  30270  chsupsn  31502  chlejb1i  31565  atsseq  32436  disjeq1f  32662  ldgenpisys  34350  measxun2  34394  measssd  34399  measiuns  34401  pmeasmono  34508  eulerpartlemb  34552  bnj1143  34972  bnj1322  35004  funsseq  35996  opnbnd  36553  cldbnd  36554  fnemeet1  36594  tz9.1tco  36711  bj-restuni  37455  bj-inexeqex  37514  bj-idreseq  37522  relowlpssretop  37726  pibt2  37779  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  heiborlem10  38187  smprngopr  38419  funALTVeq  39152  disjeq  39201  lshpcmp  39480  lsatcmp  39495  lsatcmp2  39496  lshpset2N  39611  paddasslem17  40328  pcl0bN  40415  pexmidALTN  40470  lcfrlem26  42060  lcfrlem36  42070  mapd0  42157  nacsfix  43161  minregex  43978  cbviuneq12df  44105  relexp0a  44160  relexpaddss  44162  frege124d  44205  k0004lem3  44593  dvconstbi  44778  ssin0  45503  icccncfext  46330  dvmptconst  46358  dvmptidg  46360  dvmulcncf  46368  dvdivcncf  46370  dirkercncflem2  46547  fourierdlem70  46619  fourierdlem71  46620  ovnsubaddlem1  47013  ovnhoi  47046  hspdifhsp  47059  fcoreslem4  47529  iuneqconst2  49313  iineqconst2  49314  seppsepf  49419  intubeu  49474  setrec2mpt  50187  0setrec  50194