Theorem eqimssi 3996

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 3958	. 2 ⊢ 𝐴 ⊆ 𝐴
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtri 3984	1 ⊢ 𝐴 ⊆ 𝐵

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-ss 3921

This theorem is used by:  funi  6568  fpr  7151  tz7.48-2  8427  trcl  9695  zorn2lem4  10489  zmin  12974  elfzo1  13748  om2uzf1oi  13996  0trrel  15025  sumsplit  15826  isumless  15906  rnglidl1  21369  frlmip  21939  ust0  24388  rrxprds  25559  rrxip  25560  ovoliunnul  25677  vitalilem5  25782  logtayl  26836  bdayons  28480  nbgr2vtx1edg  29711  nbuhgr2vtx1edgb  29713  mayetes3i  32092  cycpmconjslem2  33484  esplyind  33974  eulerpartlemsv2  34757  eulerpartlemsv3  34760  eulerpartlemv  34763  eulerpartlemb  34767  poimirlem9  38308  dvasin  38383  dmcoss3  39220  disjALTVid  39532  sticksstones17  42958  sticksstones18  42959  nna4b4nsq  43420  cnvrcl0  44379  corclrcl  44461  trclrelexplem  44465  cotrcltrcl  44479  he0  44538  dvsid  45069  binomcxplemnotnn0  45094  wfaxreg  45737  fourierdlem62  46910  fourierdlem66  46914  isubgr3stgrlem6  48764