Theorem eqimss2 4006

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

Assertion

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

Proof of Theorem eqimss2

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  pweq  4579  ifpprsnss  4730  unieq  4881  disjeq2  5079  disjeq1  5082  poeq2  5554  freq2  5609  seeq1  5610  seeq2  5611  dmcoeq  5934  xp11  6132  suc11  6429  funeq  6526  fimadmfoALT  6772  foco  6775  fconst3  7168  sorpssuni  7674  sorpssint  7675  tposeq  8164  oaass  8513  odi  8531  oen0  8538  mapssfset  8796  inficl  9370  fodomfi2  10005  zorng  10449  rlimclim  15440  imasaddfnlem  17424  imasvscafn  17433  gasubg  19096  pgpssslw  19410  dprddisj2  19832  dprd2da  19835  imadrhmcl  20320  evlslem6  21528  topgele  22316  topontopn  22326  connima  22813  islocfin  22905  ptbasfi  22969  txdis  23020  neifil  23268  elfm3  23338  rnelfmlem  23340  alexsubALTlem3  23437  alexsubALTlem4  23438  utopsnneiplem  23636  lmclimf  24705  uniiccdif  24979  dv11cn  25402  plypf1  25610  2pthon3v  28951  hstoh  31237  dmdi2  31309  disjeq1f  31558  eulerpartlemd  33055  rrvdmss  33138  umgr2cycllem  33821  refssfne  34906  neibastop3  34910  topmeet  34912  topjoin  34913  fnemeet2  34915  fnejoin1  34916  bj-restuni  35641  bj-inexeqex  35698  bj-idreseq  35706  heiborlem3  36345  funALTVeq  37235  disjeq  37269  lsatelbN  37541  lkrscss  37633  lshpset2N  37654  mapdrvallem2  40181  hdmaprnlem3eN  40394  hdmaplkr  40449  uneqsn  42419  ssrecnpr  42710  founiiun  43518  founiiun0  43531  caragendifcl  44875  fnfocofob  45431  imasetpreimafvbijlemfo  45717  unilbeu  47130