Theorem eqimssi 4025

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

Syntax hints:   = wceq 1537   ⊆ wss 3936

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  funi  6387  fpr  6916  tz7.48-2  8078  trcl  9170  zorn2lem4  9921  zmin  12345  elfzo1  13088  om2uzf1oi  13322  0trrel  14341  sumsplit  15123  isumless  15200  frlmip  20922  ust0  22828  rrxprds  23992  rrxip  23993  ovoliunnul  24108  vitalilem5  24213  logtayl  25243  nbgr2vtx1edg  27132  nbuhgr2vtx1edgb  27134  mayetes3i  29506  cycpmconjslem2  30797  eulerpartlemsv2  31616  eulerpartlemsv3  31619  eulerpartlemv  31622  eulerpartlemb  31626  poimirlem9  34916  dvasin  34993  dmcoss3  35708  disjALTVid  36000  cnvrcl0  40005  corclrcl  40072  trclrelexplem  40076  cotrcltrcl  40090  he0  40150  dvsid  40683  binomcxplemnotnn0  40708  fourierdlem62  42473  fourierdlem66  42477