Theorem eqimss 4042

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  eqimss2  4043  sspss  4102  uneqin  4289  difn0  4367  ssdisj  4460  uneqdifeq  4493  pweq  4614  pwpw0  4813  ssprsseq  4825  sssn  4826  snsspw  4844  unieq  4918  unissint  4972  pwpwssunieq  5104  elpwuni  5105  disjeq2  5114  disjeq1  5117  pwne  5353  pwssun  5575  poeq2  5596  freq2  5653  seeq1  5655  seeq2  5656  frsn  5773  dmxpss  6191  xp11  6195  dmsnopss  6234  trsucss  6472  suc11  6491  iotassuni  6533  iotassuniOLD  6540  funeq  6586  fnresdm  6687  fssxp  6763  ffdm  6765  fcoi1  6782  fof  6820  dff1o2  6853  fvmptss  7028  fvmptss2  7042  funressn  7179  dff1o6  7295  sucexeloniOLD  7830  suceloniOLD  7832  tposeq  8253  tfrlem11  8428  oewordi  8629  oewordri  8630  dffi3  9471  cantnfle  9711  cantnflem2  9730  r1ord3g  9819  rankeq0b  9900  rankxplim3  9921  carddom2  10017  cflm  10290  cfsuc  10297  isf32lem2  10394  axdc3lem2  10491  ttukeylem5  10553  tsksuc  10802  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  xptrrel  15019  relexpnndm  15080  relexpdmg  15081  relexprng  15085  relexpfld  15088  relexpaddg  15092  invf  17812  sscres  17867  pgpssslw  19632  fislw  19643  frgpup1  19793  frgpup3lem  19795  dprdspan  20047  dprdz  20050  dprdf1o  20052  dprd2da  20062  ablfac1b  20090  lspsncmp  21118  lspsnne2  21120  lspsneq  21124  psgnghm2  21599  psrbaglesupp  21942  psrbaglefi  21946  mplcoe5  22058  mplbas2  22060  ofco2  22457  toprntopon  22931  cncnpi  23286  hauscmplem  23414  iskgen2  23556  elqtop3  23711  qtoprest  23725  hmeores  23779  snfil  23872  uffixfr  23931  ustuqtop2  24251  tngngp2  24673  metnrmlem3  24883  volcn  25641  recnprss  25939  plyeq0  26250  madebdaylemlrcut  27937  uhgr3cyclex  30201  chsupsn  31432  chlejb1i  31495  atsseq  32366  disjeq1f  32586  ldgenpisys  34167  measxun2  34211  measssd  34216  measiuns  34218  pmeasmono  34326  eulerpartlemb  34370  bnj1143  34804  bnj1322  34836  funsseq  35768  opnbnd  36326  cldbnd  36327  fnemeet1  36367  bj-restuni  37098  bj-inexeqex  37155  bj-idreseq  37163  relowlpssretop  37365  pibt2  37418  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  heiborlem10  37827  smprngopr  38059  funALTVeq  38701  disjeq  38735  lshpcmp  38989  lsatcmp  39004  lsatcmp2  39005  lshpset2N  39120  paddasslem17  39838  pcl0bN  39925  pexmidALTN  39980  lcfrlem26  41570  lcfrlem36  41580  mapd0  41667  nacsfix  42723  minregex  43547  cbviuneq12df  43674  relexp0a  43729  relexpaddss  43731  frege124d  43774  k0004lem3  44162  dvconstbi  44353  ssin0  45060  icccncfext  45902  dvmptconst  45930  dvmptidg  45932  dvmulcncf  45940  dvdivcncf  45942  dirkercncflem2  46119  fourierdlem70  46191  fourierdlem71  46192  hoicvr  46563  ovnsubaddlem1  46585  ovnhoi  46618  hspdifhsp  46631  fcoreslem4  47078  seppsepf  48826  intubeu  48873  setrec2mpt  49216  0setrec  49223