Theorem eqimss 4067

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqimss2  4068  sspss  4125  uneqin  4308  difn0  4390  ssdisj  4483  uneqdifeq  4516  pweq  4636  pwpw0  4838  ssprsseq  4850  sssn  4851  snsspw  4869  unieq  4942  unissint  4996  pwpwssunieq  5127  elpwuni  5128  disjeq2  5137  disjeq1  5140  pwne  5371  pwssun  5590  poeq2  5611  freq2  5668  seeq1  5670  seeq2  5671  frsn  5787  dmxpss  6202  xp11  6206  dmsnopss  6245  trsucss  6483  suc11  6502  iotassuni  6545  iotassuniOLD  6552  funeq  6598  fnresdm  6699  fssxp  6775  ffdm  6777  fcoi1  6795  fof  6834  dff1o2  6867  fvmptss  7041  fvmptss2  7055  funressn  7193  dff1o6  7311  sucexeloniOLD  7846  suceloniOLD  7848  tposeq  8269  tfrlem11  8444  oewordi  8647  oewordri  8648  dffi3  9500  cantnfle  9740  cantnflem2  9759  r1ord3g  9848  rankeq0b  9929  rankxplim3  9950  carddom2  10046  cflm  10319  cfsuc  10326  isf32lem2  10423  axdc3lem2  10520  ttukeylem5  10582  tsksuc  10831  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  xptrrel  15029  relexpnndm  15090  relexpdmg  15091  relexprng  15095  relexpfld  15098  relexpaddg  15102  invf  17829  sscres  17884  pgpssslw  19656  fislw  19667  frgpup1  19817  frgpup3lem  19819  dprdspan  20071  dprdz  20074  dprdf1o  20076  dprd2da  20086  ablfac1b  20114  lspsncmp  21141  lspsnne2  21143  lspsneq  21147  psgnghm2  21622  psrbaglesupp  21965  psrbaglefi  21969  mplcoe5  22081  mplbas2  22083  ofco2  22478  toprntopon  22952  cncnpi  23307  hauscmplem  23435  iskgen2  23577  elqtop3  23732  qtoprest  23746  hmeores  23800  snfil  23893  uffixfr  23952  ustuqtop2  24272  tngngp2  24694  metnrmlem3  24902  volcn  25660  recnprss  25959  plyeq0  26270  madebdaylemlrcut  27955  uhgr3cyclex  30214  chsupsn  31445  chlejb1i  31508  atsseq  32379  disjeq1f  32595  ldgenpisys  34130  measxun2  34174  measssd  34179  measiuns  34181  pmeasmono  34289  eulerpartlemb  34333  bnj1143  34766  bnj1322  34798  funsseq  35731  opnbnd  36291  cldbnd  36292  fnemeet1  36332  bj-restuni  37063  bj-inexeqex  37120  bj-idreseq  37128  relowlpssretop  37330  pibt2  37383  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  heiborlem10  37780  smprngopr  38012  funALTVeq  38656  disjeq  38690  lshpcmp  38944  lsatcmp  38959  lsatcmp2  38960  lshpset2N  39075  paddasslem17  39793  pcl0bN  39880  pexmidALTN  39935  lcfrlem26  41525  lcfrlem36  41535  mapd0  41622  nacsfix  42668  minregex  43496  cbviuneq12df  43623  relexp0a  43678  relexpaddss  43680  frege124d  43723  k0004lem3  44111  dvconstbi  44303  ssin0  44957  icccncfext  45808  dvmptconst  45836  dvmptidg  45838  dvmulcncf  45846  dvdivcncf  45848  dirkercncflem2  46025  fourierdlem70  46097  fourierdlem71  46098  hoicvr  46469  ovnsubaddlem1  46491  ovnhoi  46524  hspdifhsp  46537  fcoreslem4  46981  seppsepf  48608  intubeu  48656  setrec2mpt  48789  0setrec  48796