Theorem eqimss 3156

Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
eqimss	⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 3117	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2	1	simplbi 272	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1332   ⊆ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  eqimss2  3157  uneqin  3332  sssnr  3688  sssnm  3689  ssprr  3691  sstpr  3692  snsspw  3699  pwpwssunieq  3909  elpwuni  3910  disjeq2  3918  disjeq1  3921  pwne  4092  pwssunim  4214  poeq2  4230  seeq1  4269  seeq2  4270  trsucss  4353  onsucelsucr  4432  xp11m  4985  funeq  5151  fnresdm  5240  fssxp  5298  ffdm  5301  fcoi1  5311  fof  5353  dff1o2  5380  fvmptss2  5504  fvmptssdm  5513  fprg  5611  dff1o6  5685  tposeq  6152  nntri1  6400  nntri2or2  6402  nnsseleq  6405  infnninf  7030  frec2uzf1od  10210  hashinfuni  10555  setsresg  12036  setsslid  12048  strle1g  12088  cncnpi  12436  hmeores  12523  limcimolemlt  12841  recnprss  12864  el2oss1o  13359  0nninf  13372  nninfall  13379