Theorem eqimss2 3981

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  pweq  4555  ifpprsnss  4708  unieq  4861  disjeq2  5056  disjeq1  5059  poeq2  5543  freq2  5599  seeq1  5601  seeq2  5602  dmcoeq  5936  xp11  6139  suc11  6432  funeq  6518  fimadmfoALT  6763  foco  6766  fconst3  7168  sorpssuni  7686  sorpssint  7687  tposeq  8178  oaass  8496  odi  8514  oen0  8522  mapssfset  8798  inficl  9338  fodomfi2  9982  zorng  10426  rlimclim  15508  imasaddfnlem  17492  imasvscafn  17501  gasubg  19277  pgpssslw  19589  dprddisj2  20016  dprd2da  20019  imadrhmcl  20774  evlslem6  22059  topgele  22895  topontopn  22905  connima  23390  islocfin  23482  ptbasfi  23546  txdis  23597  neifil  23845  elfm3  23915  rnelfmlem  23917  alexsubALTlem3  24014  alexsubALTlem4  24015  utopsnneiplem  24212  lmclimf  25271  uniiccdif  25545  dv11cn  25968  plypf1  26177  2pthon3v  30011  hstoh  32303  dmdi2  32375  disjeq1f  32643  eulerpartlemd  34510  rrvdmss  34593  umgr2cycllem  35322  refssfne  36540  neibastop3  36544  topmeet  36546  topjoin  36547  fnemeet2  36549  fnejoin1  36550  bj-restuni  37409  bj-inexeqex  37468  bj-idreseq  37476  heiborlem3  38134  funALTVeq  39106  disjeq  39155  lsatelbN  39452  lkrscss  39544  lshpset2N  39565  mapdrvallem2  42091  hdmaprnlem3eN  42304  hdmaplkr  42359  uneqsn  44452  ssrecnpr  44735  founiiun  45609  founiiun0  45620  caragendifcl  46942  fnfocofob  47527  imasetpreimafvbijlemfo  47865  iuneqconst2  49298  iineqconst2  49299  unilbeu  49460