Theorem eqimss2 3990

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

Assertion

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

Proof of Theorem eqimss2

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  pweq  4571  ifpprsnss  4725  unieq  4878  disjeq2  5074  disjeq1  5077  poeq2  5567  freq2  5623  seeq1  5625  seeq2  5626  dmcoeq  5964  xp11  6168  suc11  6467  funeq  6553  fimadmfoALT  6801  foco  6804  fconst3  7213  sorpssuni  7734  sorpssint  7735  tposeq  8227  oaass  8549  odi  8567  oen0  8575  mapssfset  8853  inficl  9396  fodomfi2  10064  zorng  10507  rlimclim  15634  imasaddfnlem  17615  imasvscafn  17624  gasubg  19430  pgpssslw  19742  dprddisj2  20169  dprd2da  20172  imadrhmcl  20964  evlslem6  22298  topgele  23156  topontopn  23166  connima  23651  islocfin  23744  ptbasfi  23808  txdis  23859  neifil  24107  elfm3  24177  rnelfmlem  24179  alexsubALTlem3  24276  alexsubALTlem4  24277  utopsnneiplem  24474  lmclimf  25533  uniiccdif  25807  dv11cn  26229  plypf1  26439  2pthon3v  30412  umgr2cycllem  30626  hstoh  32714  dmdi2  32786  disjeq1f  33047  eulerpartlemd  34878  rrvdmss  34961  refssfne  36978  neibastop3  36982  topmeet  36984  topjoin  36985  fnemeet2  36987  fnejoin1  36988  bj-restuni  37848  bj-inexeqex  37907  bj-idreseq  37915  heiborlem3  38564  funALTVeq  39534  disjeq  39583  lsatelbN  39880  lkrscss  39972  lshpset2N  39993  mapdrvallem2  42519  hdmaprnlem3eN  42732  hdmaplkr  42787  uneqsn  44866  ssrecnpr  45133  founiiun  46012  founiiun0  46023  caragendifcl  47343  fnfocofob  47968  imasetpreimafvbijlemfo  48306  iuneqconst2  49752  iineqconst2  49753  unilbeu  49912