Theorem eqimss2 3997

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

Assertion

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

Proof of Theorem eqimss2

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  pweq  4578  ifpprsnss  4732  unieq  4885  disjeq2  5082  disjeq1  5085  poeq2  5575  freq2  5631  seeq1  5633  seeq2  5634  dmcoeq  5972  xp11  6175  suc11  6474  funeq  6560  fimadmfoALT  6807  foco  6810  fconst3  7218  sorpssuni  7739  sorpssint  7740  tposeq  8230  oaass  8552  odi  8570  oen0  8578  mapssfset  8854  inficl  9392  fodomfi2  10060  zorng  10503  rlimclim  15621  imasaddfnlem  17604  imasvscafn  17613  gasubg  19416  pgpssslw  19728  dprddisj2  20155  dprd2da  20158  imadrhmcl  20950  evlslem6  22282  topgele  23137  topontopn  23147  connima  23632  islocfin  23725  ptbasfi  23789  txdis  23840  neifil  24088  elfm3  24158  rnelfmlem  24160  alexsubALTlem3  24257  alexsubALTlem4  24258  utopsnneiplem  24455  lmclimf  25514  uniiccdif  25788  dv11cn  26211  plypf1  26420  2pthon3v  30359  umgr2cycllem  30573  hstoh  32655  dmdi2  32727  disjeq1f  32989  eulerpartlemd  34821  rrvdmss  34904  refssfne  36926  neibastop3  36930  topmeet  36932  topjoin  36933  fnemeet2  36935  fnejoin1  36936  bj-restuni  37796  bj-inexeqex  37855  bj-idreseq  37863  heiborlem3  38522  funALTVeq  39492  disjeq  39541  lsatelbN  39838  lkrscss  39930  lshpset2N  39951  mapdrvallem2  42477  hdmaprnlem3eN  42690  hdmaplkr  42745  uneqsn  44809  ssrecnpr  45076  founiiun  45955  founiiun0  45966  caragendifcl  47286  fnfocofob  47874  imasetpreimafvbijlemfo  48212  iuneqconst2  49658  iineqconst2  49659  unilbeu  49820