Theorem eqimss2 4043

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  pweq  4614  ifpprsnss  4764  unieq  4918  disjeq2  5114  disjeq1  5117  poeq2  5596  freq2  5653  seeq1  5655  seeq2  5656  dmcoeq  5989  xp11  6195  suc11  6491  funeq  6586  fimadmfoALT  6831  foco  6834  fconst3  7233  sorpssuni  7752  sorpssint  7753  tposeq  8253  oaass  8599  odi  8617  oen0  8624  mapssfset  8891  inficl  9465  fodomfi2  10100  zorng  10544  rlimclim  15582  imasaddfnlem  17573  imasvscafn  17582  gasubg  19320  pgpssslw  19632  dprddisj2  20059  dprd2da  20062  imadrhmcl  20798  evlslem6  22105  topgele  22936  topontopn  22946  connima  23433  islocfin  23525  ptbasfi  23589  txdis  23640  neifil  23888  elfm3  23958  rnelfmlem  23960  alexsubALTlem3  24057  alexsubALTlem4  24058  utopsnneiplem  24256  lmclimf  25338  uniiccdif  25613  dv11cn  26040  plypf1  26251  2pthon3v  29963  hstoh  32251  dmdi2  32323  disjeq1f  32586  eulerpartlemd  34368  rrvdmss  34451  umgr2cycllem  35145  refssfne  36359  neibastop3  36363  topmeet  36365  topjoin  36366  fnemeet2  36368  fnejoin1  36369  bj-restuni  37098  bj-inexeqex  37155  bj-idreseq  37163  heiborlem3  37820  funALTVeq  38701  disjeq  38735  lsatelbN  39007  lkrscss  39099  lshpset2N  39120  mapdrvallem2  41647  hdmaprnlem3eN  41860  hdmaplkr  41915  uneqsn  44038  ssrecnpr  44327  founiiun  45184  founiiun0  45195  caragendifcl  46529  fnfocofob  47091  imasetpreimafvbijlemfo  47392  unilbeu  48874