Theorem eqimss2 3971

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

Assertion

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

Proof of Theorem eqimss2

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ss 3900

This theorem is used by:  pweq  4573  ifpprsnss  4724  unieq  4880  disjeq2  5076  disjeq1  5079  poeq2  5566  freq2  5622  seeq1  5624  seeq2  5625  dmcoeq  5966  xp11  6172  suc11  6478  funeq  6567  fimadmfoALT  6815  foco  6818  fconst3  7226  sorpssuni  7755  sorpssint  7756  tposeq  8256  oaass  8580  odi  8598  oen0  8606  mapssfset  8884  inficl  9427  fodomfi2  10149  zorng  10592  rlimclim  15725  imasaddfnlem  17712  imasvscafn  17721  gasubg  19528  pgpssslw  19840  dprddisj2  20267  dprd2da  20270  imadrhmcl  21066  evlslem6  22402  topgele  23260  topontopn  23270  connima  23755  islocfin  23848  ptbasfi  23912  txdis  23963  neifil  24211  elfm3  24281  rnelfmlem  24283  alexsubALTlem3  24380  alexsubALTlem4  24381  utopsnneiplem  24578  lmclimf  25637  uniiccdif  25911  dv11cn  26333  plypf1  26543  2pthon3v  30544  umgr2cycllem  30758  hstoh  32846  dmdi2  32918  disjeq1f  33221  eulerpartlemd  35051  rrvdmss  35134  refssfne  37273  neibastop3  37277  topmeet  37279  topjoin  37280  fnemeet2  37282  fnejoin1  37283  bj-restuni  38157  bj-inexeqex  38215  bj-idreseq  38223  heiborlem3  38887  funALTVeq  39857  disjeq  39906  lsatelbN  40203  lkrscss  40295  lshpset2N  40316  mapdrvallem2  42842  hdmaprnlem3eN  43055  hdmaplkr  43110  uneqsn  45165  ssrecnpr  45432  founiiun  46333  founiiun0  46344  caragendifcl  47663  fnfocofob  48288  imasetpreimafvbijlemfo  48626  iuneqconst2  50073  iineqconst2  50074  unilbeu  50238