Theorem eqimss2 3978

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  pweq  4549  ifpprsnss  4700  unieq  4850  disjeq2  5043  disjeq1  5046  poeq2  5507  freq2  5560  seeq1  5561  seeq2  5562  dmcoeq  5883  xp11  6078  suc11  6369  funeq  6454  fimadmfoALT  6699  foco  6702  fconst3  7089  sorpssuni  7585  sorpssint  7586  tposeq  8044  oaass  8392  odi  8410  oen0  8417  mapssfset  8639  inficl  9184  fodomfi2  9816  zorng  10260  rlimclim  15255  imasaddfnlem  17239  imasvscafn  17248  gasubg  18908  pgpssslw  19219  dprddisj2  19642  dprd2da  19645  evlslem6  21291  topgele  22079  topontopn  22089  connima  22576  islocfin  22668  ptbasfi  22732  txdis  22783  neifil  23031  elfm3  23101  rnelfmlem  23103  alexsubALTlem3  23200  alexsubALTlem4  23201  utopsnneiplem  23399  lmclimf  24468  uniiccdif  24742  dv11cn  25165  plypf1  25373  2pthon3v  28308  hstoh  30594  dmdi2  30666  disjeq1f  30912  eulerpartlemd  32333  rrvdmss  32416  umgr2cycllem  33102  refssfne  34547  neibastop3  34551  topmeet  34553  topjoin  34554  fnemeet2  34556  fnejoin1  34557  bj-restuni  35268  bj-inexeqex  35325  bj-idreseq  35333  heiborlem3  35971  funALTVeq  36811  disjeq  36845  lsatelbN  37020  lkrscss  37112  lshpset2N  37133  mapdrvallem2  39659  hdmaprnlem3eN  39872  hdmaplkr  39927  uneqsn  41633  ssrecnpr  41926  founiiun  42715  founiiun0  42728  caragendifcl  44052  fnfocofob  44571  imasetpreimafvbijlemfo  44857  unilbeu  46271