Theorem eqimss2 3989

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

Assertion

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

Proof of Theorem eqimss2

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  pweq  4561  ifpprsnss  4714  unieq  4867  disjeq2  5060  disjeq1  5063  poeq2  5526  freq2  5582  seeq1  5584  seeq2  5585  dmcoeq  5919  xp11  6122  suc11  6415  funeq  6501  fimadmfoALT  6746  foco  6749  fconst3  7147  sorpssuni  7665  sorpssint  7666  tposeq  8158  oaass  8476  odi  8494  oen0  8501  mapssfset  8775  inficl  9309  fodomfi2  9951  zorng  10395  rlimclim  15453  imasaddfnlem  17432  imasvscafn  17441  gasubg  19214  pgpssslw  19526  dprddisj2  19953  dprd2da  19956  imadrhmcl  20712  evlslem6  22016  topgele  22845  topontopn  22855  connima  23340  islocfin  23432  ptbasfi  23496  txdis  23547  neifil  23795  elfm3  23865  rnelfmlem  23867  alexsubALTlem3  23964  alexsubALTlem4  23965  utopsnneiplem  24162  lmclimf  25231  uniiccdif  25506  dv11cn  25933  plypf1  26144  2pthon3v  29921  hstoh  32212  dmdi2  32284  disjeq1f  32553  eulerpartlemd  34379  rrvdmss  34462  umgr2cycllem  35184  refssfne  36400  neibastop3  36404  topmeet  36406  topjoin  36407  fnemeet2  36409  fnejoin1  36410  bj-restuni  37139  bj-inexeqex  37196  bj-idreseq  37204  heiborlem3  37861  funALTVeq  38746  disjeq  38780  lsatelbN  39053  lkrscss  39145  lshpset2N  39166  mapdrvallem2  41692  hdmaprnlem3eN  41905  hdmaplkr  41960  uneqsn  44066  ssrecnpr  44349  founiiun  45224  founiiun0  45235  caragendifcl  46560  fnfocofob  47118  imasetpreimafvbijlemfo  47444  iuneqconst2  48862  iineqconst2  48863  unilbeu  49024