Theorem eqimss2 4009

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  pweq  4580  ifpprsnss  4731  unieq  4885  disjeq2  5081  disjeq1  5084  poeq2  5553  freq2  5609  seeq1  5611  seeq2  5612  dmcoeq  5945  xp11  6151  suc11  6444  funeq  6539  fimadmfoALT  6786  foco  6789  fconst3  7190  sorpssuni  7711  sorpssint  7712  tposeq  8210  oaass  8528  odi  8546  oen0  8553  mapssfset  8827  inficl  9383  fodomfi2  10020  zorng  10464  rlimclim  15519  imasaddfnlem  17498  imasvscafn  17507  gasubg  19241  pgpssslw  19551  dprddisj2  19978  dprd2da  19981  imadrhmcl  20713  evlslem6  21995  topgele  22824  topontopn  22834  connima  23319  islocfin  23411  ptbasfi  23475  txdis  23526  neifil  23774  elfm3  23844  rnelfmlem  23846  alexsubALTlem3  23943  alexsubALTlem4  23944  utopsnneiplem  24142  lmclimf  25211  uniiccdif  25486  dv11cn  25913  plypf1  26124  2pthon3v  29880  hstoh  32168  dmdi2  32240  disjeq1f  32509  eulerpartlemd  34364  rrvdmss  34447  umgr2cycllem  35134  refssfne  36353  neibastop3  36357  topmeet  36359  topjoin  36360  fnemeet2  36362  fnejoin1  36363  bj-restuni  37092  bj-inexeqex  37149  bj-idreseq  37157  heiborlem3  37814  funALTVeq  38699  disjeq  38733  lsatelbN  39006  lkrscss  39098  lshpset2N  39119  mapdrvallem2  41646  hdmaprnlem3eN  41859  hdmaplkr  41914  uneqsn  44021  ssrecnpr  44304  founiiun  45180  founiiun0  45191  caragendifcl  46519  fnfocofob  47084  imasetpreimafvbijlemfo  47410  iuneqconst2  48815  iineqconst2  48816  unilbeu  48977