Theorem eqimssi 3991

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  funi  6561  fpr  7147  tz7.48-2  8431  trcl  9707  zorn2lem4  10534  zmin  13026  elfzo1  13801  om2uzf1oi  14050  0trrel  15087  sumsplit  15887  isumless  15967  rnglidl1  21459  frlmip  22031  ust0  24486  rrxprds  25657  rrxip  25658  ovoliunnul  25775  vitalilem5  25880  logtayl  26937  bdayons  28581  nbgr2vtx1edg  29850  nbuhgr2vtx1edgb  29852  mayetes3i  32250  cycpmconjslem2  33635  esplyind  34126  eulerpartlemsv2  34910  eulerpartlemsv3  34913  eulerpartlemv  34916  eulerpartlemb  34920  poimirlem9  38461  dvasin  38536  dmcoss3  39389  disjALTVid  39701  sticksstones17  43127  sticksstones18  43128  nna4b4nsq  43604  cnvrcl0  44563  corclrcl  44645  trclrelexplem  44649  cotrcltrcl  44663  he0  44722  dvsid  45253  binomcxplemnotnn0  45278  wfaxreg  45921  fourierdlem62  47094  fourierdlem66  47098  isubgr3stgrlem6  48985