Theorem eqimss2 3982

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  pweq  4556  ifpprsnss  4709  unieq  4862  disjeq2  5057  disjeq1  5060  poeq2  5537  freq2  5593  seeq1  5595  seeq2  5596  dmcoeq  5931  xp11  6134  suc11  6427  funeq  6513  fimadmfoALT  6758  foco  6761  fconst3  7162  sorpssuni  7680  sorpssint  7681  tposeq  8172  oaass  8490  odi  8508  oen0  8516  mapssfset  8792  inficl  9332  fodomfi2  9976  zorng  10420  rlimclim  15502  imasaddfnlem  17486  imasvscafn  17495  gasubg  19271  pgpssslw  19583  dprddisj2  20010  dprd2da  20013  imadrhmcl  20768  evlslem6  22072  topgele  22908  topontopn  22918  connima  23403  islocfin  23495  ptbasfi  23559  txdis  23610  neifil  23858  elfm3  23928  rnelfmlem  23930  alexsubALTlem3  24027  alexsubALTlem4  24028  utopsnneiplem  24225  lmclimf  25284  uniiccdif  25558  dv11cn  25981  plypf1  26190  2pthon3v  30029  hstoh  32321  dmdi2  32393  disjeq1f  32661  eulerpartlemd  34529  rrvdmss  34612  umgr2cycllem  35341  refssfne  36559  neibastop3  36563  topmeet  36565  topjoin  36566  fnemeet2  36568  fnejoin1  36569  bj-restuni  37428  bj-inexeqex  37487  bj-idreseq  37495  heiborlem3  38151  funALTVeq  39123  disjeq  39172  lsatelbN  39469  lkrscss  39561  lshpset2N  39582  mapdrvallem2  42108  hdmaprnlem3eN  42321  hdmaplkr  42376  uneqsn  44473  ssrecnpr  44756  founiiun  45630  founiiun0  45641  caragendifcl  46963  fnfocofob  47542  imasetpreimafvbijlemfo  47880  iuneqconst2  49313  iineqconst2  49314  unilbeu  49475