Theorem eqimss2 3974

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

Assertion

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

Proof of Theorem eqimss2

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  pweq  4546  ifpprsnss  4697  unieq  4847  disjeq2  5039  disjeq1  5042  poeq2  5498  freq2  5551  seeq1  5552  seeq2  5553  dmcoeq  5872  xp11  6067  suc11  6354  funeq  6438  fimadmfoALT  6683  foco  6686  fconst3  7071  sorpssuni  7563  sorpssint  7564  tposeq  8015  oaass  8354  odi  8372  oen0  8379  mapssfset  8597  inficl  9114  fodomfi2  9747  zorng  10191  rlimclim  15183  imasaddfnlem  17156  imasvscafn  17165  gasubg  18823  pgpssslw  19134  dprddisj2  19557  dprd2da  19560  evlslem6  21201  topgele  21987  topontopn  21997  connima  22484  islocfin  22576  ptbasfi  22640  txdis  22691  neifil  22939  elfm3  23009  rnelfmlem  23011  alexsubALTlem3  23108  alexsubALTlem4  23109  utopsnneiplem  23307  lmclimf  24373  uniiccdif  24647  dv11cn  25070  plypf1  25278  2pthon3v  28209  hstoh  30495  dmdi2  30567  disjeq1f  30813  eulerpartlemd  32233  rrvdmss  32316  umgr2cycllem  33002  refssfne  34474  neibastop3  34478  topmeet  34480  topjoin  34481  fnemeet2  34483  fnejoin1  34484  bj-restuni  35195  bj-inexeqex  35252  bj-idreseq  35260  heiborlem3  35898  funALTVeq  36738  disjeq  36772  lsatelbN  36947  lkrscss  37039  lshpset2N  37060  mapdrvallem2  39586  hdmaprnlem3eN  39799  hdmaplkr  39854  uneqsn  41522  ssrecnpr  41815  founiiun  42604  founiiun0  42617  caragendifcl  43942  fnfocofob  44458  imasetpreimafvbijlemfo  44745  unilbeu  46159