Theorem eqimss2 4006

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

Assertion

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

Proof of Theorem eqimss2

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  pweq  4577  ifpprsnss  4728  unieq  4882  disjeq2  5078  disjeq1  5081  poeq2  5550  freq2  5606  seeq1  5608  seeq2  5609  dmcoeq  5942  xp11  6148  suc11  6441  funeq  6536  fimadmfoALT  6783  foco  6786  fconst3  7187  sorpssuni  7708  sorpssint  7709  tposeq  8207  oaass  8525  odi  8543  oen0  8550  mapssfset  8824  inficl  9376  fodomfi2  10013  zorng  10457  rlimclim  15512  imasaddfnlem  17491  imasvscafn  17500  gasubg  19234  pgpssslw  19544  dprddisj2  19971  dprd2da  19974  imadrhmcl  20706  evlslem6  21988  topgele  22817  topontopn  22827  connima  23312  islocfin  23404  ptbasfi  23468  txdis  23519  neifil  23767  elfm3  23837  rnelfmlem  23839  alexsubALTlem3  23936  alexsubALTlem4  23937  utopsnneiplem  24135  lmclimf  25204  uniiccdif  25479  dv11cn  25906  plypf1  26117  2pthon3v  29873  hstoh  32161  dmdi2  32233  disjeq1f  32502  eulerpartlemd  34357  rrvdmss  34440  umgr2cycllem  35127  refssfne  36346  neibastop3  36350  topmeet  36352  topjoin  36353  fnemeet2  36355  fnejoin1  36356  bj-restuni  37085  bj-inexeqex  37142  bj-idreseq  37150  heiborlem3  37807  funALTVeq  38692  disjeq  38726  lsatelbN  38999  lkrscss  39091  lshpset2N  39112  mapdrvallem2  41639  hdmaprnlem3eN  41852  hdmaplkr  41907  uneqsn  44014  ssrecnpr  44297  founiiun  45173  founiiun0  45184  caragendifcl  46512  fnfocofob  47080  imasetpreimafvbijlemfo  47406  iuneqconst2  48811  iineqconst2  48812  unilbeu  48973