Theorem eqimss 4036

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961

This theorem is referenced by:  eqimss2  4037  sspss  4095  uneqin  4274  difn0  4360  ssdisj  4455  uneqdifeq  4486  pweq  4610  pwpw0  4809  ssprsseq  4821  sssn  4822  snsspw  4838  pwsnOLD  4894  unieq  4912  unissint  4969  pwpwssunieq  5100  elpwuni  5101  disjeq2  5110  disjeq1  5113  pwne  5343  pwssun  5564  poeq2  5585  freq2  5640  seeq1  5641  seeq2  5642  frsn  5755  dmxpss  6159  xp11  6163  dmsnopss  6202  trsucss  6441  suc11  6460  iotassuni  6504  iotassuniOLD  6511  funeq  6557  fnresdm  6656  fssxp  6732  ffdm  6734  fcoi1  6752  fof  6792  dff1o2  6825  fvmptss  6996  fvmptss2  7009  funressn  7141  dff1o6  7257  sucexeloniOLD  7781  suceloniOLD  7783  tposeq  8195  tfrlem11  8370  oewordi  8574  oewordri  8575  dffi3  9408  cantnfle  9648  cantnflem2  9667  r1ord3g  9756  rankeq0b  9837  rankxplim3  9858  carddom2  9954  cflm  10227  cfsuc  10234  isf32lem2  10331  axdc3lem2  10428  ttukeylem5  10490  tsksuc  10739  fsuppmapnn0fiublem  13937  fsuppmapnn0fiub  13938  xptrrel  14909  relexpnndm  14970  relexpdmg  14971  relexprng  14975  relexpfld  14978  relexpaddg  14982  invf  17697  sscres  17752  pgpssslw  19446  fislw  19457  frgpup1  19607  frgpup3lem  19609  dprdspan  19856  dprdz  19859  dprdf1o  19861  dprd2da  19871  ablfac1b  19899  lspsncmp  20678  lspsnne2  20680  lspsneq  20684  psgnghm2  21067  psrbaglesupp  21408  psrbaglesuppOLD  21409  psrbaglefi  21416  psrbaglefiOLD  21417  mplcoe5  21523  mplbas2  21525  ofco2  21882  toprntopon  22356  cncnpi  22711  hauscmplem  22839  iskgen2  22981  elqtop3  23136  qtoprest  23150  hmeores  23204  snfil  23297  uffixfr  23356  ustuqtop2  23676  tngngp2  24098  metnrmlem3  24306  volcn  25052  recnprss  25350  plyeq0  25654  madebdaylemlrcut  27316  uhgr3cyclex  29300  chsupsn  30529  chlejb1i  30592  atsseq  31463  disjeq1f  31669  ldgenpisys  32995  measxun2  33039  measssd  33044  measiuns  33046  pmeasmono  33154  eulerpartlemb  33198  bnj1143  33632  bnj1322  33664  funsseq  34569  opnbnd  35014  cldbnd  35015  fnemeet1  35055  bj-restuni  35782  bj-inexeqex  35839  bj-idreseq  35847  relowlpssretop  36049  pibt2  36102  ovoliunnfl  36334  voliunnfl  36336  volsupnfl  36337  heiborlem10  36493  smprngopr  36725  funALTVeq  37375  disjeq  37409  lshpcmp  37663  lsatcmp  37678  lsatcmp2  37679  lshpset2N  37794  paddasslem17  38512  pcl0bN  38599  pexmidALTN  38654  lcfrlem26  40244  lcfrlem36  40254  mapd0  40341  nacsfix  41221  minregex  42056  cbviuneq12df  42183  relexp0a  42238  relexpaddss  42240  frege124d  42283  k0004lem3  42671  dvconstbi  42864  ssin0  43513  icccncfext  44376  dvmptconst  44404  dvmptidg  44406  dvmulcncf  44414  dvdivcncf  44416  dirkercncflem2  44593  fourierdlem70  44665  fourierdlem71  44666  hoicvr  45037  ovnsubaddlem1  45059  ovnhoi  45092  hspdifhsp  45105  fcoreslem4  45548  seppsepf  47209  intubeu  47257  setrec2mpt  47390  0setrec  47397