Theorem eqimss2 3996

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  pweq  4576  ifpprsnss  4730  unieq  4883  disjeq2  5080  disjeq1  5083  poeq2  5573  freq2  5629  seeq1  5631  seeq2  5632  dmcoeq  5970  xp11  6173  suc11  6470  funeq  6556  fimadmfoALT  6803  foco  6806  fconst3  7211  sorpssuni  7729  sorpssint  7730  tposeq  8220  oaass  8542  odi  8560  oen0  8568  mapssfset  8844  inficl  9381  fodomfi2  10040  zorng  10483  rlimclim  15593  imasaddfnlem  17577  imasvscafn  17586  gasubg  19367  pgpssslw  19679  dprddisj2  20106  dprd2da  20109  imadrhmcl  20900  evlslem6  22232  topgele  23087  topontopn  23097  connima  23582  islocfin  23674  ptbasfi  23738  txdis  23789  neifil  24037  elfm3  24107  rnelfmlem  24109  alexsubALTlem3  24206  alexsubALTlem4  24207  utopsnneiplem  24404  lmclimf  25463  uniiccdif  25737  dv11cn  26160  plypf1  26369  2pthon3v  30292  hstoh  32584  dmdi2  32656  disjeq1f  32918  eulerpartlemd  34756  rrvdmss  34839  umgr2cycllem  35632  refssfne  36869  neibastop3  36873  topmeet  36875  topjoin  36876  fnemeet2  36878  fnejoin1  36879  bj-restuni  37739  bj-inexeqex  37798  bj-idreseq  37806  heiborlem3  38464  funALTVeq  39434  disjeq  39483  lsatelbN  39780  lkrscss  39872  lshpset2N  39893  mapdrvallem2  42419  hdmaprnlem3eN  42632  hdmaplkr  42687  uneqsn  44751  ssrecnpr  45018  founiiun  45897  founiiun0  45908  caragendifcl  47228  fnfocofob  47816  imasetpreimafvbijlemfo  48154  iuneqconst2  49601  iineqconst2  49602  unilbeu  49763