Theorem eqimss 3980

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqimss2  3981  sspss  4042  uneqin  4229  difn0  4307  ssdisj  4400  uneqdifeq  4432  pweq  4555  pwpw0  4756  ssprsseq  4768  sssn  4769  snsspw  4787  unieq  4861  unissint  4914  pwpwssunieq  5046  elpwuni  5047  disjeq2  5056  disjeq1  5059  pwne  5294  pwssun  5523  poeq2  5543  freq2  5599  seeq1  5601  seeq2  5602  frsn  5719  dmxpss  6135  xp11  6139  dmsnopss  6178  trsucss  6413  suc11  6432  iotassuni  6473  funeq  6518  fnresdm  6617  fssxp  6695  ffdm  6697  fcoi1  6714  fof  6752  dff1o2  6785  fvmptss  6960  fvmptss2  6974  funressn  7113  dff1o6  7230  tposeq  8178  tfrlem11  8327  oewordi  8527  oewordri  8528  dffi3  9344  cantnfle  9592  cantnflem2  9611  r1ord3g  9703  rankeq0b  9784  rankxplim3  9805  carddom2  9901  cflm  10172  cfsuc  10179  isf32lem2  10276  axdc3lem2  10373  ttukeylem5  10435  tsksuc  10685  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  xptrrel  14942  relexpnndm  15003  relexpdmg  15004  relexprng  15008  relexpfld  15011  relexpaddg  15015  invf  17735  sscres  17790  pgpssslw  19589  fislw  19600  frgpup1  19750  frgpup3lem  19752  dprdspan  20004  dprdz  20007  dprdf1o  20009  dprd2da  20019  ablfac1b  20047  lspsncmp  21114  lspsnne2  21116  lspsneq  21120  psgnghm2  21561  psrbaglesupp  21902  psrbaglefi  21906  mplcoe5  22018  mplbas2  22020  ofco2  22416  toprntopon  22890  cncnpi  23243  hauscmplem  23371  iskgen2  23513  elqtop3  23668  qtoprest  23682  hmeores  23736  snfil  23829  uffixfr  23888  ustuqtop2  24207  tngngp2  24617  metnrmlem3  24827  volcn  25573  recnprss  25871  plyeq0  26176  madebdaylemlrcut  27891  uhgr3cyclex  30252  chsupsn  31484  chlejb1i  31547  atsseq  32418  disjeq1f  32643  ldgenpisys  34310  measxun2  34354  measssd  34359  measiuns  34361  pmeasmono  34468  eulerpartlemb  34512  bnj1143  34932  bnj1322  34964  funsseq  35950  opnbnd  36507  cldbnd  36508  fnemeet1  36548  tz9.1tco  36665  bj-restuni  37409  bj-inexeqex  37468  bj-idreseq  37476  relowlpssretop  37680  pibt2  37733  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  heiborlem10  38141  smprngopr  38373  funALTVeq  39106  disjeq  39155  lshpcmp  39434  lsatcmp  39449  lsatcmp2  39450  lshpset2N  39565  paddasslem17  40282  pcl0bN  40369  pexmidALTN  40424  lcfrlem26  42014  lcfrlem36  42024  mapd0  42111  nacsfix  43144  minregex  43961  cbviuneq12df  44088  relexp0a  44143  relexpaddss  44145  frege124d  44188  k0004lem3  44576  dvconstbi  44761  ssin0  45486  icccncfext  46315  dvmptconst  46343  dvmptidg  46345  dvmulcncf  46353  dvdivcncf  46355  dirkercncflem2  46532  fourierdlem70  46604  fourierdlem71  46605  ovnsubaddlem1  46998  ovnhoi  47031  hspdifhsp  47044  fcoreslem4  47514  iuneqconst2  49298  iineqconst2  49299  seppsepf  49404  intubeu  49459  setrec2mpt  50172  0setrec  50179