Theorem eqimssi 3982

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

Syntax hints:   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  funi  6530  fpr  7108  tz7.48-2  8381  trcl  9649  zorn2lem4  10421  zmin  12894  elfzo1  13667  om2uzf1oi  13915  0trrel  14943  sumsplit  15730  isumless  15810  rnglidl1  21230  frlmip  21758  ust0  24185  rrxprds  25356  rrxip  25357  ovoliunnul  25474  vitalilem5  25579  logtayl  26624  bdayons  28268  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  mayetes3i  31800  cycpmconjslem2  33216  esplyind  33719  eulerpartlemsv2  34502  eulerpartlemsv3  34505  eulerpartlemv  34508  eulerpartlemb  34512  poimirlem9  37950  dvasin  38025  dmcoss3  38864  disjALTVid  39176  sticksstones17  42602  sticksstones18  42603  nna4b4nsq  43093  cnvrcl0  44052  corclrcl  44134  trclrelexplem  44138  cotrcltrcl  44152  he0  44211  dvsid  44758  binomcxplemnotnn0  44783  wfaxreg  45427  fourierdlem62  46596  fourierdlem66  46600  isubgr3stgrlem6  48447