Theorem eqimssi 4043

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

Syntax hints:   = wceq 1539   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

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

This theorem is referenced by:  funi  6597  fpr  7173  tz7.48-2  8483  trcl  9769  zorn2lem4  10540  zmin  12987  elfzo1  13753  om2uzf1oi  13995  0trrel  15021  sumsplit  15805  isumless  15882  rnglidl1  21243  frlmip  21799  ust0  24229  rrxprds  25424  rrxip  25425  ovoliunnul  25543  vitalilem5  25648  logtayl  26703  nbgr2vtx1edg  29368  nbuhgr2vtx1edgb  29370  mayetes3i  31749  cycpmconjslem2  33176  eulerpartlemsv2  34361  eulerpartlemsv3  34364  eulerpartlemv  34367  eulerpartlemb  34371  poimirlem9  37637  dvasin  37712  dmcoss3  38455  disjALTVid  38757  sticksstones17  42165  sticksstones18  42166  nna4b4nsq  42675  cnvrcl0  43643  corclrcl  43725  trclrelexplem  43729  cotrcltrcl  43743  he0  43802  dvsid  44355  binomcxplemnotnn0  44380  wfaxreg  45022  fourierdlem62  46188  fourierdlem66  46192  isubgr3stgrlem6  47943