Theorem eqimss2 4004

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  pweq  4581  ifpprsnss  4735  unieq  4887  disjeq2  5084  disjeq1  5087  poeq2  5574  freq2  5630  seeq1  5632  seeq2  5633  dmcoeq  5971  xp11  6174  suc11  6471  funeq  6557  fimadmfoALT  6804  foco  6807  fconst3  7212  sorpssuni  7730  sorpssint  7731  tposeq  8223  oaass  8545  odi  8563  oen0  8571  mapssfset  8847  inficl  9384  fodomfi2  10043  zorng  10487  rlimclim  15596  imasaddfnlem  17581  imasvscafn  17590  gasubg  19371  pgpssslw  19683  dprddisj2  20110  dprd2da  20113  imadrhmcl  20877  evlslem6  22200  topgele  23055  topontopn  23065  connima  23550  islocfin  23642  ptbasfi  23706  txdis  23757  neifil  24005  elfm3  24075  rnelfmlem  24077  alexsubALTlem3  24174  alexsubALTlem4  24175  utopsnneiplem  24372  lmclimf  25431  uniiccdif  25705  dv11cn  26128  plypf1  26337  2pthon3v  30232  hstoh  32524  dmdi2  32596  disjeq1f  32858  eulerpartlemd  34700  rrvdmss  34783  umgr2cycllem  35530  refssfne  36757  neibastop3  36761  topmeet  36763  topjoin  36764  fnemeet2  36766  fnejoin1  36767  bj-restuni  37626  bj-inexeqex  37685  bj-idreseq  37693  heiborlem3  38351  funALTVeq  39323  disjeq  39372  lsatelbN  39669  lkrscss  39761  lshpset2N  39782  mapdrvallem2  42308  hdmaprnlem3eN  42521  hdmaplkr  42576  uneqsn  44642  ssrecnpr  44909  founiiun  45788  founiiun0  45799  caragendifcl  47119  fnfocofob  47704  imasetpreimafvbijlemfo  48042  iuneqconst2  49485  iineqconst2  49486  unilbeu  49647