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 4019	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  funi  6581  fpr  7152  tz7.48-2  8442  trcl  9723  zorn2lem4  10494  zmin  12928  elfzo1  13682  om2uzf1oi  13918  0trrel  14928  sumsplit  15714  isumless  15791  frlmip  21333  ust0  23724  rrxprds  24906  rrxip  24907  ovoliunnul  25024  vitalilem5  25129  logtayl  26168  nbgr2vtx1edg  28638  nbuhgr2vtx1edgb  28640  mayetes3i  31013  cycpmconjslem2  32345  eulerpartlemsv2  33388  eulerpartlemsv3  33391  eulerpartlemv  33394  eulerpartlemb  33398  poimirlem9  36545  dvasin  36620  dmcoss3  37371  disjALTVid  37673  sticksstones17  41027  sticksstones18  41028  nna4b4nsq  41450  cnvrcl0  42424  corclrcl  42506  trclrelexplem  42510  cotrcltrcl  42524  he0  42583  dvsid  43138  binomcxplemnotnn0  43163  fourierdlem62  44932  fourierdlem66  44936  rnglidl1  46801