Theorem eqimss2 3990

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

Assertion

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

Proof of Theorem eqimss2

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  pweq  4571  ifpprsnss  4725  unieq  4878  disjeq2  5074  disjeq1  5077  poeq2  5563  freq2  5619  seeq1  5621  seeq2  5622  dmcoeq  5962  xp11  6167  suc11  6472  funeq  6559  fimadmfoALT  6807  foco  6810  fconst3  7219  sorpssuni  7748  sorpssint  7749  tposeq  8245  oaass  8569  odi  8587  oen0  8595  mapssfset  8873  inficl  9417  fodomfi2  10139  zorng  10582  rlimclim  15713  imasaddfnlem  17700  imasvscafn  17709  gasubg  19516  pgpssslw  19828  dprddisj2  20255  dprd2da  20258  imadrhmcl  21054  evlslem6  22390  topgele  23248  topontopn  23258  connima  23743  islocfin  23836  ptbasfi  23900  txdis  23951  neifil  24199  elfm3  24269  rnelfmlem  24271  alexsubALTlem3  24368  alexsubALTlem4  24369  utopsnneiplem  24566  lmclimf  25625  uniiccdif  25899  dv11cn  26321  plypf1  26531  2pthon3v  30532  umgr2cycllem  30746  hstoh  32834  dmdi2  32906  disjeq1f  33167  eulerpartlemd  34998  rrvdmss  35081  refssfne  37146  neibastop3  37150  topmeet  37152  topjoin  37153  fnemeet2  37155  fnejoin1  37156  bj-restuni  38018  bj-inexeqex  38075  bj-idreseq  38083  heiborlem3  38747  funALTVeq  39717  disjeq  39766  lsatelbN  40063  lkrscss  40155  lshpset2N  40176  mapdrvallem2  42702  hdmaprnlem3eN  42915  hdmaplkr  42970  uneqsn  45024  ssrecnpr  45291  founiiun  46193  founiiun0  46204  caragendifcl  47523  fnfocofob  48148  imasetpreimafvbijlemfo  48486  iuneqconst2  49932  iineqconst2  49933  unilbeu  50092