Theorem eqimss 3279

Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

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

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 3240	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2	1	simplbi 274	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  eqimss2  3280  uneqin  3456  ssprsseq  3833  sssnr  3834  sssnm  3835  ssprr  3837  sstpr  3838  snsspw  3845  pwpwssunieq  4057  elpwuni  4058  disjeq2  4066  disjeq1  4069  pwne  4248  pwssunim  4379  poeq2  4395  seeq1  4434  seeq2  4435  trsucss  4518  onsucelsucr  4604  xp11m  5173  funeq  5344  fnresdm  5438  fssxp  5499  ffdm  5502  fcoi1  5514  fof  5556  dff1o2  5585  fvmptss2  5717  fvmptssdm  5727  fprg  5832  dff1o6  5912  tposeq  6408  el2oss1o  6606  nntri1  6659  nntri2or2  6661  nnsseleq  6664  infnninf  7314  infnninfOLD  7315  nninfwlpoimlemg  7365  exmidontri2or  7451  frec2uzf1od  10658  hashinfuni  11029  setsresg  13110  setsslid  13123  strle1g  13179  cncnpi  14942  hmeores  15029  limcimolemlt  15378  recnprss  15401  plycoeid3  15471  0nninf  16542  nninfall  16547