Theorem eqimss 3996

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqimssd 3994	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  eqimss2  3997  sspss  4057  uneqin  4242  difn0  4322  ssdisj  4420  uneqdifeq  4455  pweq  4578  pwpw0  4781  ssprsseq  4793  sssn  4794  snsspw  4811  unieq  4885  unissint  4939  pwpwssunieq  5072  elpwuni  5073  disjeq2  5082  disjeq1  5085  pwne  5325  pwssun  5555  poeq2  5575  freq2  5631  seeq1  5633  seeq2  5634  frsn  5751  dmxpss  6171  xp11  6175  dmsnopss  6217  trsucss  6455  suc11  6474  iotassuni  6515  funeq  6560  fnresdm  6658  fssxp  6737  ffdm  6739  fcoi1  6756  fof  6796  dff1o2  6830  fvmptss  7006  fvmptss2  7020  funressn  7162  dff1o6  7282  tposeq  8230  tfrlem11  8381  oewordi  8583  oewordri  8584  dffi3  9398  cantnfle  9647  cantnflem2  9666  r1ord3g  9758  rankeq0b  9839  rankxplim3  9860  carddom2  9979  cflm  10248  cfsuc  10256  isf32lem2  10353  axdc3lem2  10450  ttukeylem5  10512  tsksuc  10762  fsuppmapnn0fiublem  14044  fsuppmapnn0fiub  14045  xptrrel  15041  relexpnndm  15102  relexpdmg  15103  relexprng  15107  relexpfld  15110  relexpaddg  15114  invf  17847  sscres  17902  pgpssslw  19728  fislw  19739  frgpup1  19889  frgpup3lem  19891  dprdspan  20143  dprdz  20146  dprdf1o  20148  dprd2da  20158  ablfac1b  20186  lspsncmp  21290  lspsnne2  21292  lspsneq  21296  psgnghm2  21781  psrbaglesupp  22122  psrbaglefi  22126  mplcoe5  22241  mplbas2  22243  ofco2  22658  toprntopon  23132  cncnpi  23485  hauscmplem  23613  iskgen2  23756  elqtop3  23911  qtoprest  23925  hmeores  23979  snfil  24072  uffixfr  24131  ustuqtop2  24450  tngngp2  24860  metnrmlem3  25070  volcn  25816  recnprss  26114  plyeq0  26419  madebdaylemlrcut  28143  uhgr3cyclex  30604  chsupsn  31836  chlejb1i  31899  atsseq  32770  disjeq1f  32989  ldgenpisys  34621  measxun2  34665  measssd  34670  measiuns  34672  pmeasmono  34779  eulerpartlemb  34823  bnj1143  35243  bnj1322  35275  fnfvintima  35535  funsseq  36297  opnbnd  36893  cldbnd  36894  fnemeet1  36934  tz9.1tco  37051  bj-restuni  37796  bj-inexeqex  37855  bj-idreseq  37863  relowlpssretop  38067  pibt2  38120  ovoliunnfl  38370  voliunnfl  38372  volsupnfl  38373  heiborlem10  38529  smprngopr  38761  funALTVeq  39492  disjeq  39541  lshpcmp  39820  lsatcmp  39835  lsatcmp2  39836  lshpset2N  39951  paddasslem17  40668  pcl0bN  40755  pexmidALTN  40810  lcfrlem26  42400  lcfrlem36  42410  mapd0  42497  nacsfix  43501  minregex  44318  cbviuneq12df  44445  relexp0a  44500  relexpaddss  44502  frege124d  44545  k0004lem3  44933  dvconstbi  45102  ssin0  45833  icccncfext  46659  dvmptconst  46687  dvmptidg  46689  dvmulcncf  46697  dvdivcncf  46699  dirkercncflem2  46876  fourierdlem70  46948  fourierdlem71  46949  ovnsubaddlem1  47342  ovnhoi  47375  hspdifhsp  47388  fcoreslem4  47861  smprngprmrng  49161  iuneqconst2  49658  iineqconst2  49659  seppsepf  49764  intubeu  49819  setrec2mpt  50532  0setrec  50539