Theorem eqimss 4037

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3945

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3952  df-ss 3962

This theorem is referenced by:  eqimss2  4038  sspss  4096  uneqin  4275  difn0  4361  ssdisj  4456  uneqdifeq  4487  pweq  4611  pwpw0  4810  ssprsseq  4822  sssn  4823  snsspw  4839  pwsnOLD  4895  unieq  4913  unissint  4970  pwpwssunieq  5101  elpwuni  5102  disjeq2  5111  disjeq1  5114  pwne  5344  pwssun  5565  poeq2  5586  freq2  5641  seeq1  5642  seeq2  5643  frsn  5756  dmxpss  6160  xp11  6164  dmsnopss  6203  trsucss  6442  suc11  6461  iotassuni  6505  iotassuniOLD  6512  funeq  6558  fnresdm  6657  fssxp  6733  ffdm  6735  fcoi1  6753  fof  6793  dff1o2  6826  fvmptss  6997  fvmptss2  7010  funressn  7142  dff1o6  7258  sucexeloniOLD  7782  suceloniOLD  7784  tposeq  8197  tfrlem11  8372  oewordi  8576  oewordri  8577  dffi3  9410  cantnfle  9650  cantnflem2  9669  r1ord3g  9758  rankeq0b  9839  rankxplim3  9860  carddom2  9956  cflm  10229  cfsuc  10236  isf32lem2  10333  axdc3lem2  10430  ttukeylem5  10492  tsksuc  10741  fsuppmapnn0fiublem  13939  fsuppmapnn0fiub  13940  xptrrel  14911  relexpnndm  14972  relexpdmg  14973  relexprng  14977  relexpfld  14980  relexpaddg  14984  invf  17699  sscres  17754  pgpssslw  19448  fislw  19459  frgpup1  19609  frgpup3lem  19611  dprdspan  19858  dprdz  19861  dprdf1o  19863  dprd2da  19873  ablfac1b  19901  lspsncmp  20680  lspsnne2  20682  lspsneq  20686  psgnghm2  21069  psrbaglesupp  21410  psrbaglesuppOLD  21411  psrbaglefi  21418  psrbaglefiOLD  21419  mplcoe5  21525  mplbas2  21527  ofco2  21884  toprntopon  22358  cncnpi  22713  hauscmplem  22841  iskgen2  22983  elqtop3  23138  qtoprest  23152  hmeores  23206  snfil  23299  uffixfr  23358  ustuqtop2  23678  tngngp2  24100  metnrmlem3  24308  volcn  25054  recnprss  25352  plyeq0  25656  madebdaylemlrcut  27322  uhgr3cyclex  29364  chsupsn  30593  chlejb1i  30656  atsseq  31527  disjeq1f  31733  ldgenpisys  33059  measxun2  33103  measssd  33108  measiuns  33110  pmeasmono  33218  eulerpartlemb  33262  bnj1143  33696  bnj1322  33728  funsseq  34633  opnbnd  35078  cldbnd  35079  fnemeet1  35119  bj-restuni  35846  bj-inexeqex  35903  bj-idreseq  35911  relowlpssretop  36113  pibt2  36166  ovoliunnfl  36398  voliunnfl  36400  volsupnfl  36401  heiborlem10  36557  smprngopr  36789  funALTVeq  37439  disjeq  37473  lshpcmp  37727  lsatcmp  37742  lsatcmp2  37743  lshpset2N  37858  paddasslem17  38576  pcl0bN  38663  pexmidALTN  38718  lcfrlem26  40308  lcfrlem36  40318  mapd0  40405  nacsfix  41285  minregex  42120  cbviuneq12df  42247  relexp0a  42302  relexpaddss  42304  frege124d  42347  k0004lem3  42735  dvconstbi  42928  ssin0  43577  icccncfext  44440  dvmptconst  44468  dvmptidg  44470  dvmulcncf  44478  dvdivcncf  44480  dirkercncflem2  44657  fourierdlem70  44729  fourierdlem71  44730  hoicvr  45101  ovnsubaddlem1  45123  ovnhoi  45156  hspdifhsp  45169  fcoreslem4  45612  seppsepf  47273  intubeu  47321  setrec2mpt  47454  0setrec  47461