Theorem eqimss2 3995

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920

This theorem is referenced by:  pweq  4565  ifpprsnss  4716  unieq  4869  disjeq2  5063  disjeq1  5066  poeq2  5531  freq2  5587  seeq1  5589  seeq2  5590  dmcoeq  5922  xp11  6124  suc11  6416  funeq  6502  fimadmfoALT  6747  foco  6750  fconst3  7149  sorpssuni  7668  sorpssint  7669  tposeq  8161  oaass  8479  odi  8497  oen0  8504  mapssfset  8778  inficl  9315  fodomfi2  9954  zorng  10398  rlimclim  15453  imasaddfnlem  17432  imasvscafn  17441  gasubg  19181  pgpssslw  19493  dprddisj2  19920  dprd2da  19923  imadrhmcl  20682  evlslem6  21986  topgele  22815  topontopn  22825  connima  23310  islocfin  23402  ptbasfi  23466  txdis  23517  neifil  23765  elfm3  23835  rnelfmlem  23837  alexsubALTlem3  23934  alexsubALTlem4  23935  utopsnneiplem  24133  lmclimf  25202  uniiccdif  25477  dv11cn  25904  plypf1  26115  2pthon3v  29888  hstoh  32176  dmdi2  32248  disjeq1f  32517  eulerpartlemd  34334  rrvdmss  34417  umgr2cycllem  35113  refssfne  36332  neibastop3  36336  topmeet  36338  topjoin  36339  fnemeet2  36341  fnejoin1  36342  bj-restuni  37071  bj-inexeqex  37128  bj-idreseq  37136  heiborlem3  37793  funALTVeq  38678  disjeq  38712  lsatelbN  38985  lkrscss  39077  lshpset2N  39098  mapdrvallem2  41624  hdmaprnlem3eN  41837  hdmaplkr  41892  uneqsn  43998  ssrecnpr  44281  founiiun  45157  founiiun0  45168  caragendifcl  46495  fnfocofob  47063  imasetpreimafvbijlemfo  47389  iuneqconst2  48807  iineqconst2  48808  unilbeu  48969