Theorem eqimss 4053

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqimss2  4054  sspss  4111  uneqin  4294  difn0  4372  ssdisj  4465  uneqdifeq  4498  pweq  4618  pwpw0  4817  ssprsseq  4829  sssn  4830  snsspw  4848  unieq  4922  unissint  4976  pwpwssunieq  5108  elpwuni  5109  disjeq2  5118  disjeq1  5121  pwne  5358  pwssun  5579  poeq2  5600  freq2  5656  seeq1  5658  seeq2  5659  frsn  5775  dmxpss  6192  xp11  6196  dmsnopss  6235  trsucss  6473  suc11  6492  iotassuni  6534  iotassuniOLD  6541  funeq  6587  fnresdm  6687  fssxp  6763  ffdm  6765  fcoi1  6782  fof  6820  dff1o2  6853  fvmptss  7027  fvmptss2  7041  funressn  7178  dff1o6  7294  sucexeloniOLD  7829  suceloniOLD  7831  tposeq  8251  tfrlem11  8426  oewordi  8627  oewordri  8628  dffi3  9468  cantnfle  9708  cantnflem2  9727  r1ord3g  9816  rankeq0b  9897  rankxplim3  9918  carddom2  10014  cflm  10287  cfsuc  10294  isf32lem2  10391  axdc3lem2  10488  ttukeylem5  10550  tsksuc  10799  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  xptrrel  15015  relexpnndm  15076  relexpdmg  15077  relexprng  15081  relexpfld  15084  relexpaddg  15088  invf  17815  sscres  17870  pgpssslw  19646  fislw  19657  frgpup1  19807  frgpup3lem  19809  dprdspan  20061  dprdz  20064  dprdf1o  20066  dprd2da  20076  ablfac1b  20104  lspsncmp  21135  lspsnne2  21137  lspsneq  21141  psgnghm2  21616  psrbaglesupp  21959  psrbaglefi  21963  mplcoe5  22075  mplbas2  22077  ofco2  22472  toprntopon  22946  cncnpi  23301  hauscmplem  23429  iskgen2  23571  elqtop3  23726  qtoprest  23740  hmeores  23794  snfil  23887  uffixfr  23946  ustuqtop2  24266  tngngp2  24688  metnrmlem3  24896  volcn  25654  recnprss  25953  plyeq0  26264  madebdaylemlrcut  27951  uhgr3cyclex  30210  chsupsn  31441  chlejb1i  31504  atsseq  32375  disjeq1f  32592  ldgenpisys  34146  measxun2  34190  measssd  34195  measiuns  34197  pmeasmono  34305  eulerpartlemb  34349  bnj1143  34782  bnj1322  34814  funsseq  35748  opnbnd  36307  cldbnd  36308  fnemeet1  36348  bj-restuni  37079  bj-inexeqex  37136  bj-idreseq  37144  relowlpssretop  37346  pibt2  37399  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  heiborlem10  37806  smprngopr  38038  funALTVeq  38681  disjeq  38715  lshpcmp  38969  lsatcmp  38984  lsatcmp2  38985  lshpset2N  39100  paddasslem17  39818  pcl0bN  39905  pexmidALTN  39960  lcfrlem26  41550  lcfrlem36  41560  mapd0  41647  nacsfix  42699  minregex  43523  cbviuneq12df  43650  relexp0a  43705  relexpaddss  43707  frege124d  43750  k0004lem3  44138  dvconstbi  44329  ssin0  44994  icccncfext  45842  dvmptconst  45870  dvmptidg  45872  dvmulcncf  45880  dvdivcncf  45882  dirkercncflem2  46059  fourierdlem70  46131  fourierdlem71  46132  hoicvr  46503  ovnsubaddlem1  46525  ovnhoi  46558  hspdifhsp  46571  fcoreslem4  47015  seppsepf  48724  intubeu  48772  setrec2mpt  48927  0setrec  48934