Theorem eqimss 2975

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

Assertion

Ref	Expression
eqimss	⊢ (A = B → A ⊆ B)

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 2938	. 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
2	1	simplbi 259	1 ⊢ (A = B → A ⊆ B)

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 2895

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-8 1377  ax-11 1379  ax-4 1382  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-nf 1329  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2902  df-ss 2909

This theorem is referenced by:  eqimss2  2976  sspssr  3021  sspsstrir  3024  uneqin  3166  sssnr  3476  sssnm  3477  ssprr  3479  sstpr  3480  snsspw  3487  elpwuni  3693  disjeq2  3701  disjeq1  3704  pwne  3865  pwssunim  3974  poeq2  3990  seeq1  4019  seeq2  4020  trsucss  4083  onsucelsucr  4156  xp11m  4653  funeq  4814  fnresdm  4901  fssxp  4950  ffdm  4953  fcoi1  4962  fof  4998  dff1o2  5023  fvmptss2  5139  fvmptssdm  5147  fprg  5238  dff1o6  5308  tposeq  5750