Theorem eqimss2 4041

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  pweq  4616  ifpprsnss  4768  unieq  4919  disjeq2  5117  disjeq1  5120  poeq2  5592  freq2  5647  seeq1  5648  seeq2  5649  dmcoeq  5973  xp11  6174  suc11  6471  funeq  6568  fimadmfoALT  6816  foco  6819  fconst3  7217  sorpssuni  7724  sorpssint  7725  tposeq  8215  oaass  8563  odi  8581  oen0  8588  mapssfset  8847  inficl  9422  fodomfi2  10057  zorng  10501  rlimclim  15492  imasaddfnlem  17476  imasvscafn  17485  gasubg  19168  pgpssslw  19484  dprddisj2  19911  dprd2da  19914  imadrhmcl  20417  evlslem6  21650  topgele  22439  topontopn  22449  connima  22936  islocfin  23028  ptbasfi  23092  txdis  23143  neifil  23391  elfm3  23461  rnelfmlem  23463  alexsubALTlem3  23560  alexsubALTlem4  23561  utopsnneiplem  23759  lmclimf  24828  uniiccdif  25102  dv11cn  25525  plypf1  25733  2pthon3v  29235  hstoh  31523  dmdi2  31595  disjeq1f  31842  eulerpartlemd  33434  rrvdmss  33517  umgr2cycllem  34200  refssfne  35329  neibastop3  35333  topmeet  35335  topjoin  35336  fnemeet2  35338  fnejoin1  35339  bj-restuni  36064  bj-inexeqex  36121  bj-idreseq  36129  heiborlem3  36767  funALTVeq  37656  disjeq  37690  lsatelbN  37962  lkrscss  38054  lshpset2N  38075  mapdrvallem2  40602  hdmaprnlem3eN  40815  hdmaplkr  40870  uneqsn  42858  ssrecnpr  43149  founiiun  43957  founiiun0  43968  caragendifcl  45309  fnfocofob  45866  imasetpreimafvbijlemfo  46152  unilbeu  47688