Theorem eqimssi 4069

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  funi  6610  fpr  7188  tz7.48-2  8498  trcl  9797  zorn2lem4  10568  zmin  13009  elfzo1  13766  om2uzf1oi  14004  0trrel  15030  sumsplit  15816  isumless  15893  rnglidl1  21265  frlmip  21821  ust0  24249  rrxprds  25442  rrxip  25443  ovoliunnul  25561  vitalilem5  25666  logtayl  26720  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  mayetes3i  31761  cycpmconjslem2  33148  eulerpartlemsv2  34323  eulerpartlemsv3  34326  eulerpartlemv  34329  eulerpartlemb  34333  poimirlem9  37589  dvasin  37664  dmcoss3  38409  disjALTVid  38711  sticksstones17  42120  sticksstones18  42121  nna4b4nsq  42615  cnvrcl0  43587  corclrcl  43669  trclrelexplem  43673  cotrcltrcl  43687  he0  43746  dvsid  44300  binomcxplemnotnn0  44325  fourierdlem62  46089  fourierdlem66  46093