Theorem eqimssi 3973

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  funi  6589  fpr  7179  tz7.48-2  8477  trcl  9753  zorn2lem4  10601  zmin  13095  elfzo1  13871  om2uzf1oi  14120  0trrel  15160  sumsplit  15960  isumless  16040  rnglidl1  21539  frlmip  22111  ust0  24566  rrxprds  25737  rrxip  25738  ovoliunnul  25855  vitalilem5  25960  logtayl  27015  nna4b4nsq  28017  bdayons  28689  nbgr2vtx1edg  29958  nbuhgr2vtx1edgb  29960  mayetes3i  32358  cycpmconjslem2  33783  esplyind  34274  eulerpartlemsv2  35057  eulerpartlemsv3  35060  eulerpartlemv  35063  eulerpartlemb  35067  poimirlem9  38738  dvasin  38813  dmcoss3  39666  disjALTVid  39978  sticksstones17  43404  sticksstones18  43405  cnvrcl0  44815  corclrcl  44897  trclrelexplem  44901  cotrcltrcl  44915  he0  44974  dvsid  45505  binomcxplemnotnn0  45530  wfaxreg  46183  fourierdlem62  47381  fourierdlem66  47385  isubgr3stgrlem6  49272