Theorem eqimss2 4036

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961

This theorem is referenced by:  pweq  4618  ifpprsnss  4770  unieq  4920  disjeq2  5118  disjeq1  5121  poeq2  5594  freq2  5649  seeq1  5650  seeq2  5651  dmcoeq  5977  xp11  6181  suc11  6478  funeq  6574  fimadmfoALT  6821  foco  6824  fconst3  7225  sorpssuni  7738  sorpssint  7739  tposeq  8234  oaass  8582  odi  8600  oen0  8607  mapssfset  8870  inficl  9450  fodomfi2  10085  zorng  10529  rlimclim  15526  imasaddfnlem  17513  imasvscafn  17522  gasubg  19265  pgpssslw  19581  dprddisj2  20008  dprd2da  20011  imadrhmcl  20697  evlslem6  22049  topgele  22876  topontopn  22886  connima  23373  islocfin  23465  ptbasfi  23529  txdis  23580  neifil  23828  elfm3  23898  rnelfmlem  23900  alexsubALTlem3  23997  alexsubALTlem4  23998  utopsnneiplem  24196  lmclimf  25276  uniiccdif  25551  dv11cn  25978  plypf1  26191  2pthon3v  29826  hstoh  32114  dmdi2  32186  disjeq1f  32442  eulerpartlemd  34117  rrvdmss  34200  umgr2cycllem  34881  refssfne  35973  neibastop3  35977  topmeet  35979  topjoin  35980  fnemeet2  35982  fnejoin1  35983  bj-restuni  36707  bj-inexeqex  36764  bj-idreseq  36772  heiborlem3  37417  funALTVeq  38302  disjeq  38336  lsatelbN  38608  lkrscss  38700  lshpset2N  38721  mapdrvallem2  41248  hdmaprnlem3eN  41461  hdmaplkr  41516  uneqsn  43597  ssrecnpr  43887  founiiun  44691  founiiun0  44702  caragendifcl  46040  fnfocofob  46597  imasetpreimafvbijlemfo  46882  unilbeu  48182