Theorem eqimss2 4054

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  pweq  4618  ifpprsnss  4768  unieq  4922  disjeq2  5118  disjeq1  5121  poeq2  5600  freq2  5656  seeq1  5658  seeq2  5659  dmcoeq  5991  xp11  6196  suc11  6492  funeq  6587  fimadmfoALT  6831  foco  6834  fconst3  7232  sorpssuni  7750  sorpssint  7751  tposeq  8251  oaass  8597  odi  8615  oen0  8622  mapssfset  8889  inficl  9462  fodomfi2  10097  zorng  10541  rlimclim  15578  imasaddfnlem  17574  imasvscafn  17583  gasubg  19332  pgpssslw  19646  dprddisj2  20073  dprd2da  20076  imadrhmcl  20814  evlslem6  22122  topgele  22951  topontopn  22961  connima  23448  islocfin  23540  ptbasfi  23604  txdis  23655  neifil  23903  elfm3  23973  rnelfmlem  23975  alexsubALTlem3  24072  alexsubALTlem4  24073  utopsnneiplem  24271  lmclimf  25351  uniiccdif  25626  dv11cn  26054  plypf1  26265  2pthon3v  29972  hstoh  32260  dmdi2  32332  disjeq1f  32592  eulerpartlemd  34347  rrvdmss  34430  umgr2cycllem  35124  refssfne  36340  neibastop3  36344  topmeet  36346  topjoin  36347  fnemeet2  36349  fnejoin1  36350  bj-restuni  37079  bj-inexeqex  37136  bj-idreseq  37144  heiborlem3  37799  funALTVeq  38681  disjeq  38715  lsatelbN  38987  lkrscss  39079  lshpset2N  39100  mapdrvallem2  41627  hdmaprnlem3eN  41840  hdmaplkr  41895  uneqsn  44014  ssrecnpr  44303  founiiun  45121  founiiun0  45132  caragendifcl  46469  fnfocofob  47028  imasetpreimafvbijlemfo  47329  unilbeu  48773