Theorem eqimssi 4027

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

Syntax hints:   = wceq 1537   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  funi  6389  fpr  6918  tz7.48-2  8080  trcl  9172  zorn2lem4  9923  zmin  12347  elfzo1  13090  om2uzf1oi  13324  0trrel  14343  sumsplit  15125  isumless  15202  frlmip  20924  ust0  22830  rrxprds  23994  rrxip  23995  ovoliunnul  24110  vitalilem5  24215  logtayl  25245  nbgr2vtx1edg  27134  nbuhgr2vtx1edgb  27136  mayetes3i  29508  cycpmconjslem2  30799  eulerpartlemsv2  31618  eulerpartlemsv3  31621  eulerpartlemv  31624  eulerpartlemb  31628  poimirlem9  34903  dvasin  34980  dmcoss3  35695  disjALTVid  35987  cnvrcl0  39992  corclrcl  40059  trclrelexplem  40063  cotrcltrcl  40077  he0  40137  dvsid  40670  binomcxplemnotnn0  40695  fourierdlem62  42460  fourierdlem66  42464