Theorem eqimss2 4042

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

Assertion

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

Proof of Theorem eqimss2

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  pweq  4617  ifpprsnss  4769  unieq  4920  disjeq2  5118  disjeq1  5121  poeq2  5593  freq2  5648  seeq1  5649  seeq2  5650  dmcoeq  5974  xp11  6175  suc11  6472  funeq  6569  fimadmfoALT  6817  foco  6820  fconst3  7215  sorpssuni  7722  sorpssint  7723  tposeq  8213  oaass  8561  odi  8579  oen0  8586  mapssfset  8845  inficl  9420  fodomfi2  10055  zorng  10499  rlimclim  15490  imasaddfnlem  17474  imasvscafn  17483  gasubg  19166  pgpssslw  19482  dprddisj2  19909  dprd2da  19912  imadrhmcl  20413  evlslem6  21644  topgele  22432  topontopn  22442  connima  22929  islocfin  23021  ptbasfi  23085  txdis  23136  neifil  23384  elfm3  23454  rnelfmlem  23456  alexsubALTlem3  23553  alexsubALTlem4  23554  utopsnneiplem  23752  lmclimf  24821  uniiccdif  25095  dv11cn  25518  plypf1  25726  2pthon3v  29197  hstoh  31485  dmdi2  31557  disjeq1f  31804  eulerpartlemd  33365  rrvdmss  33448  umgr2cycllem  34131  refssfne  35243  neibastop3  35247  topmeet  35249  topjoin  35250  fnemeet2  35252  fnejoin1  35253  bj-restuni  35978  bj-inexeqex  36035  bj-idreseq  36043  heiborlem3  36681  funALTVeq  37570  disjeq  37604  lsatelbN  37876  lkrscss  37968  lshpset2N  37989  mapdrvallem2  40516  hdmaprnlem3eN  40729  hdmaplkr  40784  uneqsn  42776  ssrecnpr  43067  founiiun  43875  founiiun0  43888  caragendifcl  45230  fnfocofob  45787  imasetpreimafvbijlemfo  46073  unilbeu  47610