Theorem eqimss2 3983

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  pweq  4555  ifpprsnss  4706  unieq  4856  disjeq2  5048  disjeq1  5051  poeq2  5508  freq2  5561  seeq1  5562  seeq2  5563  dmcoeq  5882  xp11  6077  suc11  6368  funeq  6452  fimadmfoALT  6697  foco  6700  fconst3  7086  sorpssuni  7580  sorpssint  7581  tposeq  8036  oaass  8384  odi  8402  oen0  8409  mapssfset  8631  inficl  9172  fodomfi2  9827  zorng  10271  rlimclim  15266  imasaddfnlem  17250  imasvscafn  17259  gasubg  18919  pgpssslw  19230  dprddisj2  19653  dprd2da  19656  evlslem6  21302  topgele  22090  topontopn  22100  connima  22587  islocfin  22679  ptbasfi  22743  txdis  22794  neifil  23042  elfm3  23112  rnelfmlem  23114  alexsubALTlem3  23211  alexsubALTlem4  23212  utopsnneiplem  23410  lmclimf  24479  uniiccdif  24753  dv11cn  25176  plypf1  25384  2pthon3v  28317  hstoh  30603  dmdi2  30675  disjeq1f  30921  eulerpartlemd  32342  rrvdmss  32425  umgr2cycllem  33111  refssfne  34556  neibastop3  34560  topmeet  34562  topjoin  34563  fnemeet2  34565  fnejoin1  34566  bj-restuni  35277  bj-inexeqex  35334  bj-idreseq  35342  heiborlem3  35980  funALTVeq  36820  disjeq  36854  lsatelbN  37029  lkrscss  37121  lshpset2N  37142  mapdrvallem2  39668  hdmaprnlem3eN  39881  hdmaplkr  39936  uneqsn  41615  ssrecnpr  41908  founiiun  42697  founiiun0  42710  caragendifcl  44034  fnfocofob  44550  imasetpreimafvbijlemfo  44836  unilbeu  46250