Theorem eqimss2 3974

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

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 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  pweq  4543  ifpprsnss  4696  unieq  4849  disjeq2  5043  disjeq1  5046  poeq2  5530  freq2  5586  seeq1  5588  seeq2  5589  dmcoeq  5923  xp11  6126  suc11  6419  funeq  6505  fimadmfoALT  6750  foco  6753  fconst3  7157  sorpssuni  7675  sorpssint  7676  tposeq  8168  oaass  8486  odi  8504  oen0  8512  mapssfset  8788  inficl  9328  fodomfi2  9973  zorng  10417  rlimclim  15499  imasaddfnlem  17483  imasvscafn  17492  gasubg  19268  pgpssslw  19580  dprddisj2  20007  dprd2da  20010  imadrhmcl  20769  evlslem6  22057  topgele  22913  topontopn  22923  connima  23408  islocfin  23500  ptbasfi  23564  txdis  23615  neifil  23863  elfm3  23933  rnelfmlem  23935  alexsubALTlem3  24032  alexsubALTlem4  24033  utopsnneiplem  24230  lmclimf  25289  uniiccdif  25563  dv11cn  25986  plypf1  26195  2pthon3v  30029  hstoh  32321  dmdi2  32393  disjeq1f  32662  eulerpartlemd  34550  rrvdmss  34633  umgr2cycllem  35368  refssfne  36586  neibastop3  36590  topmeet  36592  topjoin  36593  fnemeet2  36595  fnejoin1  36596  bj-restuni  37455  bj-inexeqex  37514  bj-idreseq  37522  heiborlem3  38180  funALTVeq  39152  disjeq  39201  lsatelbN  39498  lkrscss  39590  lshpset2N  39611  mapdrvallem2  42137  hdmaprnlem3eN  42350  hdmaplkr  42405  uneqsn  44469  ssrecnpr  44752  founiiun  45626  founiiun0  45637  caragendifcl  46957  fnfocofob  47542  imasetpreimafvbijlemfo  47880  iuneqconst2  49313  iineqconst2  49314  unilbeu  49475