Theorem eqimss2 3993

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

Assertion

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

Proof of Theorem eqimss2

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

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

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 2123  ax-ext 2708

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

This theorem is referenced by:  pweq  4568  ifpprsnss  4721  unieq  4874  disjeq2  5069  disjeq1  5072  poeq2  5536  freq2  5592  seeq1  5594  seeq2  5595  dmcoeq  5930  xp11  6133  suc11  6426  funeq  6512  fimadmfoALT  6757  foco  6760  fconst3  7159  sorpssuni  7677  sorpssint  7678  tposeq  8170  oaass  8488  odi  8506  oen0  8514  mapssfset  8788  inficl  9328  fodomfi2  9970  zorng  10414  rlimclim  15469  imasaddfnlem  17449  imasvscafn  17458  gasubg  19231  pgpssslw  19543  dprddisj2  19970  dprd2da  19973  imadrhmcl  20730  evlslem6  22036  topgele  22874  topontopn  22884  connima  23369  islocfin  23461  ptbasfi  23525  txdis  23576  neifil  23824  elfm3  23894  rnelfmlem  23896  alexsubALTlem3  23993  alexsubALTlem4  23994  utopsnneiplem  24191  lmclimf  25260  uniiccdif  25535  dv11cn  25962  plypf1  26173  2pthon3v  30016  hstoh  32307  dmdi2  32379  disjeq1f  32648  eulerpartlemd  34523  rrvdmss  34606  umgr2cycllem  35334  refssfne  36552  neibastop3  36556  topmeet  36558  topjoin  36559  fnemeet2  36561  fnejoin1  36562  bj-restuni  37302  bj-inexeqex  37359  bj-idreseq  37367  heiborlem3  38014  funALTVeq  38959  disjeq  38993  lsatelbN  39266  lkrscss  39358  lshpset2N  39379  mapdrvallem2  41905  hdmaprnlem3eN  42118  hdmaplkr  42173  uneqsn  44266  ssrecnpr  44549  founiiun  45423  founiiun0  45434  caragendifcl  46758  fnfocofob  47325  imasetpreimafvbijlemfo  47651  iuneqconst2  49068  iineqconst2  49069  unilbeu  49230