Theorem eqimss2 3986

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1550   ⊆ wss 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-ss 3912

This theorem is referenced by:  pweq  4559  ifpprsnss  4713  unieq  4866  disjeq2  5061  disjeq1  5064  poeq2  5548  freq2  5604  seeq1  5606  seeq2  5607  dmcoeq  5946  xp11  6146  suc11  6440  funeq  6526  fimadmfoALT  6774  foco  6777  fconst3  7182  sorpssuni  7700  sorpssint  7701  tposeq  8192  oaass  8514  odi  8532  oen0  8540  mapssfset  8817  inficl  9357  fodomfi2  10002  zorng  10447  rlimclim  15545  imasaddfnlem  17530  imasvscafn  17539  gasubg  19314  pgpssslw  19626  dprddisj2  20053  dprd2da  20056  imadrhmcl  20815  evlslem6  22103  topgele  22959  topontopn  22969  connima  23454  islocfin  23546  ptbasfi  23610  txdis  23661  neifil  23909  elfm3  23979  rnelfmlem  23981  alexsubALTlem3  24078  alexsubALTlem4  24079  utopsnneiplem  24276  lmclimf  25335  uniiccdif  25609  dv11cn  26032  plypf1  26241  2pthon3v  30078  hstoh  32370  dmdi2  32442  disjeq1f  32711  eulerpartlemd  34607  rrvdmss  34690  umgr2cycllem  35428  refssfne  36656  neibastop3  36660  topmeet  36662  topjoin  36663  fnemeet2  36665  fnejoin1  36666  bj-restuni  37525  bj-inexeqex  37584  bj-idreseq  37592  heiborlem3  38250  funALTVeq  39222  disjeq  39271  lsatelbN  39568  lkrscss  39660  lshpset2N  39681  mapdrvallem2  42207  hdmaprnlem3eN  42420  hdmaplkr  42475  uneqsn  44539  ssrecnpr  44822  founiiun  45695  founiiun0  45706  caragendifcl  47026  fnfocofob  47611  imasetpreimafvbijlemfo  47949  iuneqconst2  49382  iineqconst2  49383  unilbeu  49544