Theorem eqimss2 4018

Description: Equality implies inclusion. (Contributed by NM, 23-Nov-2003.)

Assertion

Ref	Expression
eqimss2	⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Proof of Theorem eqimss2

Step	Hyp	Ref	Expression
1		eqimss 4017	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	eqcoms 2743	1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

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

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 2707

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

This theorem is referenced by:  pweq  4589  ifpprsnss  4740  unieq  4894  disjeq2  5090  disjeq1  5093  poeq2  5565  freq2  5622  seeq1  5624  seeq2  5625  dmcoeq  5958  xp11  6164  suc11  6461  funeq  6556  fimadmfoALT  6801  foco  6804  fconst3  7205  sorpssuni  7726  sorpssint  7727  tposeq  8227  oaass  8573  odi  8591  oen0  8598  mapssfset  8865  inficl  9437  fodomfi2  10074  zorng  10518  rlimclim  15562  imasaddfnlem  17542  imasvscafn  17551  gasubg  19285  pgpssslw  19595  dprddisj2  20022  dprd2da  20025  imadrhmcl  20757  evlslem6  22039  topgele  22868  topontopn  22878  connima  23363  islocfin  23455  ptbasfi  23519  txdis  23570  neifil  23818  elfm3  23888  rnelfmlem  23890  alexsubALTlem3  23987  alexsubALTlem4  23988  utopsnneiplem  24186  lmclimf  25256  uniiccdif  25531  dv11cn  25958  plypf1  26169  2pthon3v  29925  hstoh  32213  dmdi2  32285  disjeq1f  32554  eulerpartlemd  34398  rrvdmss  34481  umgr2cycllem  35162  refssfne  36376  neibastop3  36380  topmeet  36382  topjoin  36383  fnemeet2  36385  fnejoin1  36386  bj-restuni  37115  bj-inexeqex  37172  bj-idreseq  37180  heiborlem3  37837  funALTVeq  38718  disjeq  38752  lsatelbN  39024  lkrscss  39116  lshpset2N  39137  mapdrvallem2  41664  hdmaprnlem3eN  41877  hdmaplkr  41932  uneqsn  44049  ssrecnpr  44332  founiiun  45203  founiiun0  45214  caragendifcl  46543  fnfocofob  47108  imasetpreimafvbijlemfo  47419  iuneqconst2  48801  iineqconst2  48802  unilbeu  48959