Theorem eqimss2 3992

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-ss 3917

This theorem is referenced by:  pweq  4562  ifpprsnss  4715  unieq  4868  disjeq2  5060  disjeq1  5063  poeq2  5526  freq2  5582  seeq1  5584  seeq2  5585  dmcoeq  5917  xp11  6119  suc11  6411  funeq  6497  fimadmfoALT  6742  foco  6745  fconst3  7142  sorpssuni  7660  sorpssint  7661  tposeq  8153  oaass  8471  odi  8489  oen0  8496  mapssfset  8770  inficl  9304  fodomfi2  9943  zorng  10387  rlimclim  15445  imasaddfnlem  17424  imasvscafn  17433  gasubg  19207  pgpssslw  19519  dprddisj2  19946  dprd2da  19949  imadrhmcl  20705  evlslem6  22009  topgele  22838  topontopn  22848  connima  23333  islocfin  23425  ptbasfi  23489  txdis  23540  neifil  23788  elfm3  23858  rnelfmlem  23860  alexsubALTlem3  23957  alexsubALTlem4  23958  utopsnneiplem  24155  lmclimf  25224  uniiccdif  25499  dv11cn  25926  plypf1  26137  2pthon3v  29914  hstoh  32202  dmdi2  32274  disjeq1f  32543  eulerpartlemd  34369  rrvdmss  34452  umgr2cycllem  35152  refssfne  36371  neibastop3  36375  topmeet  36377  topjoin  36378  fnemeet2  36380  fnejoin1  36381  bj-restuni  37110  bj-inexeqex  37167  bj-idreseq  37175  heiborlem3  37832  funALTVeq  38717  disjeq  38751  lsatelbN  39024  lkrscss  39116  lshpset2N  39137  mapdrvallem2  41663  hdmaprnlem3eN  41876  hdmaplkr  41931  uneqsn  44037  ssrecnpr  44320  founiiun  45195  founiiun0  45206  caragendifcl  46531  fnfocofob  47089  imasetpreimafvbijlemfo  47415  iuneqconst2  48833  iineqconst2  48834  unilbeu  48995