Theorem eqimss2 3991

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

Assertion

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

Proof of Theorem eqimss2

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  pweq  4566  ifpprsnss  4719  unieq  4872  disjeq2  5067  disjeq1  5070  poeq2  5534  freq2  5590  seeq1  5592  seeq2  5593  dmcoeq  5928  xp11  6131  suc11  6424  funeq  6510  fimadmfoALT  6755  foco  6758  fconst3  7157  sorpssuni  7675  sorpssint  7676  tposeq  8168  oaass  8486  odi  8504  oen0  8512  mapssfset  8786  inficl  9326  fodomfi2  9968  zorng  10412  rlimclim  15467  imasaddfnlem  17447  imasvscafn  17456  gasubg  19229  pgpssslw  19541  dprddisj2  19968  dprd2da  19971  imadrhmcl  20728  evlslem6  22034  topgele  22872  topontopn  22882  connima  23367  islocfin  23459  ptbasfi  23523  txdis  23574  neifil  23822  elfm3  23892  rnelfmlem  23894  alexsubALTlem3  23991  alexsubALTlem4  23992  utopsnneiplem  24189  lmclimf  25258  uniiccdif  25533  dv11cn  25960  plypf1  26171  2pthon3v  29965  hstoh  32256  dmdi2  32328  disjeq1f  32597  eulerpartlemd  34472  rrvdmss  34555  umgr2cycllem  35283  refssfne  36501  neibastop3  36505  topmeet  36507  topjoin  36508  fnemeet2  36510  fnejoin1  36511  bj-restuni  37241  bj-inexeqex  37298  bj-idreseq  37306  heiborlem3  37953  funALTVeq  38898  disjeq  38932  lsatelbN  39205  lkrscss  39297  lshpset2N  39318  mapdrvallem2  41844  hdmaprnlem3eN  42057  hdmaplkr  42112  uneqsn  44208  ssrecnpr  44491  founiiun  45365  founiiun0  45376  caragendifcl  46700  fnfocofob  47267  imasetpreimafvbijlemfo  47593  iuneqconst2  49010  iineqconst2  49011  unilbeu  49172