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 2770	1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  pweq  4569  ifpprsnss  4723  unieq  4876  disjeq2  5071  disjeq1  5074  poeq2  5559  freq2  5615  seeq1  5617  seeq2  5618  dmcoeq  5957  xp11  6161  suc11  6455  funeq  6541  fimadmfoALT  6789  foco  6792  fconst3  7197  sorpssuni  7715  sorpssint  7716  tposeq  8208  oaass  8530  odi  8548  oen0  8556  mapssfset  8832  inficl  9371  fodomfi2  10016  zorng  10461  rlimclim  15573  imasaddfnlem  17558  imasvscafn  17567  gasubg  19342  pgpssslw  19654  dprddisj2  20081  dprd2da  20084  imadrhmcl  20843  evlslem6  22131  topgele  22987  topontopn  22997  connima  23482  islocfin  23574  ptbasfi  23638  txdis  23689  neifil  23937  elfm3  24007  rnelfmlem  24009  alexsubALTlem3  24106  alexsubALTlem4  24107  utopsnneiplem  24304  lmclimf  25363  uniiccdif  25637  dv11cn  26060  plypf1  26269  2pthon3v  30140  hstoh  32432  dmdi2  32504  disjeq1f  32770  eulerpartlemd  34660  rrvdmss  34743  umgr2cycllem  35487  refssfne  36715  neibastop3  36719  topmeet  36721  topjoin  36722  fnemeet2  36724  fnejoin1  36725  bj-restuni  37584  bj-inexeqex  37643  bj-idreseq  37651  heiborlem3  38309  funALTVeq  39281  disjeq  39330  lsatelbN  39627  lkrscss  39719  lshpset2N  39740  mapdrvallem2  42266  hdmaprnlem3eN  42479  hdmaplkr  42534  uneqsn  44598  ssrecnpr  44881  founiiun  45754  founiiun0  45765  caragendifcl  47085  fnfocofob  47670  imasetpreimafvbijlemfo  48008  iuneqconst2  49441  iineqconst2  49442  unilbeu  49603