Theorem eqimss 3994

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

Syntax hints:   → wi 4   = wceq 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  eqimss2  3995  sspss  4055  uneqin  4241  difn0  4320  ssdisj  4414  uneqdifeq  4446  pweq  4569  pwpw0  4771  ssprsseq  4783  sssn  4784  snsspw  4802  unieq  4876  unissint  4930  pwpwssunieq  5061  elpwuni  5062  disjeq2  5071  disjeq1  5074  pwne  5309  pwssun  5539  poeq2  5559  freq2  5615  seeq1  5617  seeq2  5618  frsn  5735  dmxpss  6157  xp11  6161  dmsnopss  6201  trsucss  6436  suc11  6455  iotassuni  6496  funeq  6541  fnresdm  6640  fssxp  6719  ffdm  6721  fcoi1  6738  fof  6778  dff1o2  6812  fvmptss  6988  fvmptss2  7002  funressn  7142  dff1o6  7259  tposeq  8208  tfrlem11  8359  oewordi  8561  oewordri  8562  dffi3  9377  cantnfle  9626  cantnflem2  9645  r1ord3g  9737  rankeq0b  9818  rankxplim3  9839  carddom2  9935  cflm  10206  cfsuc  10214  isf32lem2  10311  axdc3lem2  10408  ttukeylem5  10470  tsksuc  10720  fsuppmapnn0fiublem  14003  fsuppmapnn0fiub  14004  xptrrel  14993  relexpnndm  15054  relexpdmg  15055  relexprng  15059  relexpfld  15062  relexpaddg  15066  invf  17801  sscres  17856  pgpssslw  19654  fislw  19665  frgpup1  19815  frgpup3lem  19817  dprdspan  20069  dprdz  20072  dprdf1o  20074  dprd2da  20084  ablfac1b  20112  lspsncmp  21183  lspsnne2  21185  lspsneq  21189  psgnghm2  21630  psrbaglesupp  21971  psrbaglefi  21975  mplcoe5  22090  mplbas2  22092  ofco2  22508  toprntopon  22982  cncnpi  23335  hauscmplem  23463  iskgen2  23605  elqtop3  23760  qtoprest  23774  hmeores  23828  snfil  23921  uffixfr  23980  ustuqtop2  24299  tngngp2  24709  metnrmlem3  24919  volcn  25665  recnprss  25963  plyeq0  26268  madebdaylemlrcut  27989  uhgr3cyclex  30381  chsupsn  31613  chlejb1i  31676  atsseq  32547  disjeq1f  32770  ldgenpisys  34460  measxun2  34504  measssd  34509  measiuns  34511  pmeasmono  34618  eulerpartlemb  34662  bnj1143  35082  bnj1322  35114  funsseq  36115  opnbnd  36682  cldbnd  36683  fnemeet1  36723  tz9.1tco  36840  bj-restuni  37584  bj-inexeqex  37643  bj-idreseq  37651  relowlpssretop  37855  pibt2  37908  ovoliunnfl  38158  voliunnfl  38160  volsupnfl  38161  heiborlem10  38316  smprngopr  38548  funALTVeq  39281  disjeq  39330  lshpcmp  39609  lsatcmp  39624  lsatcmp2  39625  lshpset2N  39740  paddasslem17  40457  pcl0bN  40544  pexmidALTN  40599  lcfrlem26  42189  lcfrlem36  42199  mapd0  42286  nacsfix  43290  minregex  44107  cbviuneq12df  44234  relexp0a  44289  relexpaddss  44291  frege124d  44334  k0004lem3  44722  dvconstbi  44907  ssin0  45632  icccncfext  46458  dvmptconst  46486  dvmptidg  46488  dvmulcncf  46496  dvdivcncf  46498  dirkercncflem2  46675  fourierdlem70  46747  fourierdlem71  46748  ovnsubaddlem1  47141  ovnhoi  47174  hspdifhsp  47187  fcoreslem4  47657  iuneqconst2  49441  iineqconst2  49442  seppsepf  49547  intubeu  49602  setrec2mpt  50315  0setrec  50322