Theorem eqimssi 3968

Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)

Hypothesis

Ref	Expression
eqimssi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqimssi	⊢ 𝐴 ⊆ 𝐵

Proof of Theorem eqimssi

Step	Hyp	Ref	Expression
1		ssid 3930	. 2 ⊢ 𝐴 ⊆ 𝐴
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtri 3956	1 ⊢ 𝐴 ⊆ 𝐵

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  funi  6572  fpr  7158  tz7.48-2  8452  trcl  9729  zorn2lem4  10577  zmin  13071  elfzo1  13847  om2uzf1oi  14096  0trrel  15134  sumsplit  15934  isumless  16014  rnglidl1  21512  frlmip  22084  ust0  24539  rrxprds  25710  rrxip  25711  ovoliunnul  25828  vitalilem5  25933  logtayl  26988  nna4b4nsq  27990  bdayons  28662  nbgr2vtx1edg  29931  nbuhgr2vtx1edgb  29933  mayetes3i  32331  cycpmconjslem2  33716  esplyind  34207  eulerpartlemsv2  34990  eulerpartlemsv3  34993  eulerpartlemv  34996  eulerpartlemb  35000  poimirlem9  38548  dvasin  38623  dmcoss3  39476  disjALTVid  39788  sticksstones17  43214  sticksstones18  43215  cnvrcl0  44625  corclrcl  44707  trclrelexplem  44711  cotrcltrcl  44725  he0  44784  dvsid  45315  binomcxplemnotnn0  45340  wfaxreg  45990  fourierdlem62  47178  fourierdlem66  47182  isubgr3stgrlem6  49069