Theorem eqimss 3967

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  eqimss2  3968  sspss  4028  uneqin  4233  difn0  4314  ssdisj  4412  uneqdifeq  4447  pweq  4570  ssprsseq  4780  sssn  4781  snsspw  4798  pwpw0  4830  unieq  4877  unissint  4931  pwpwssunieq  5063  elpwuni  5064  disjeq2  5073  disjeq1  5076  pwne  5314  pwssun  5543  poeq2  5563  freq2  5619  seeq1  5621  seeq2  5622  frsn  5740  dmxpss  6165  xp11  6169  dmsnopss  6218  trsucss  6456  suc11  6475  iotassuni  6517  funeq  6564  fnresdm  6663  fssxp  6742  ffdm  6744  fcoi1  6761  fof  6801  dff1o2  6835  fvmptss  7011  fvmptss2  7025  funressn  7168  dff1o6  7287  tposeq  8252  tfrlem11  8403  oewordi  8607  oewordri  8608  dffi3  9430  cantnfle  9679  cantnflem2  9698  r1ord3g  9793  rankeq0b  9883  rankxplim3  9905  carddom2  10065  cflm  10334  cfsuc  10342  isf32lem2  10439  axdc3lem2  10536  ttukeylem5  10598  tsksuc  10854  fsuppmapnn0fiublem  14140  fsuppmapnn0fiub  14141  xptrrel  15142  relexpnndm  15203  relexpdmg  15204  relexprng  15208  relexpfld  15211  relexpaddg  15215  invf  17952  sscres  18007  pgpssslw  19837  fislw  19848  frgpup1  19998  frgpup3lem  20000  dprdspan  20252  dprdz  20255  dprdf1o  20257  dprd2da  20267  ablfac1b  20295  lspsncmp  21403  lspsnne2  21405  lspsneq  21409  psgnghm2  21896  psrbaglesupp  22239  psrbaglefi  22243  mplcoe5  22358  mplbas2  22360  ofco2  22775  toprntopon  23252  cncnpi  23605  hauscmplem  23733  iskgen2  23876  elqtop3  24031  qtoprest  24045  hmeores  24099  snfil  24192  uffixfr  24251  ustuqtop2  24570  tngngp2  24980  metnrmlem3  25190  volcn  25936  recnprss  26233  plyeq0  26539  madebdaylemlrcut  28294  uhgr3cyclex  30792  chsupsn  32024  chlejb1i  32087  atsseq  32958  disjeq1f  33218  ldgenpisys  34849  measxun2  34893  measssd  34898  measiuns  34900  pmeasmono  35006  eulerpartlemb  35050  bnj1143  35470  bnj1322  35502  fnfvintima  35766  funsseq  36629  opnbnd  37209  cldbnd  37210  fnemeet1  37250  tz9.1tco  37367  bj-restuni  38126  bj-inexeqex  38184  bj-idreseq  38192  relowlpssretop  38396  pibt2  38449  ovoliunnfl  38689  voliunnfl  38691  volsupnfl  38692  heiborlem10  38863  smprngopr  39095  funALTVeq  39826  disjeq  39875  lshpcmp  40154  lsatcmp  40169  lsatcmp2  40170  lshpset2N  40285  paddasslem17  41002  pcl0bN  41089  pexmidALTN  41144  lcfrlem26  42734  lcfrlem36  42744  mapd0  42831  nacsfix  43832  minregex  44644  cbviuneq12df  44770  relexp0a  44825  relexpaddss  44827  frege124d  44870  k0004lem3  45258  dvconstbi  45427  ssin0  46180  icccncfext  47005  dvmptconst  47033  dvmptidg  47035  dvmulcncf  47043  dvdivcncf  47045  dirkercncflem2  47222  fourierdlem70  47294  fourierdlem71  47295  ovnsubaddlem1  47688  ovnhoi  47721  hspdifhsp  47734  fcoreslem4  48244  smprngprmrng  49544  iuneqconst2  50042  iineqconst2  50043  seppsepf  50151  intubeu  50206  setrec2mpt  50973  0setrec  50980