Theorem eqimssi 3995

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

Syntax hints:   = wceq 1542   ⊆ wss 3902

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 2709

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

This theorem is referenced by:  funi  6525  fpr  7101  tz7.48-2  8375  trcl  9641  zorn2lem4  10413  zmin  12861  elfzo1  13632  om2uzf1oi  13880  0trrel  14908  sumsplit  15695  isumless  15772  rnglidl1  21191  frlmip  21737  ust0  24168  rrxprds  25349  rrxip  25350  ovoliunnul  25468  vitalilem5  25573  logtayl  26629  bdayons  28276  nbgr2vtx1edg  29427  nbuhgr2vtx1edgb  29429  mayetes3i  31808  cycpmconjslem2  33239  esplyind  33733  eulerpartlemsv2  34517  eulerpartlemsv3  34520  eulerpartlemv  34523  eulerpartlemb  34527  poimirlem9  37832  dvasin  37907  dmcoss3  38746  disjALTVid  39058  sticksstones17  42485  sticksstones18  42486  nna4b4nsq  42970  cnvrcl0  43933  corclrcl  44015  trclrelexplem  44019  cotrcltrcl  44033  he0  44092  dvsid  44639  binomcxplemnotnn0  44664  wfaxreg  45308  fourierdlem62  46479  fourierdlem66  46483  isubgr3stgrlem6  48284