Theorem eqimss 3296

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 3257	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2	1	simplbi 274	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1398   ⊆ wss 3214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  eqimss2  3297  uneqin  3476  ssprsseq  3861  sssnr  3862  sssnm  3863  ssprr  3865  sstpr  3866  snsspw  3873  pwpwssunieq  4085  elpwuni  4086  disjeq2  4094  disjeq1  4097  pwne  4278  pwssunim  4410  poeq2  4426  seeq1  4465  seeq2  4466  trsucss  4549  onsucelsucr  4635  xp11m  5206  funeq  5377  fnresdm  5472  fssxp  5535  ffdm  5538  fcoi1  5552  fof  5595  dff1o2  5624  fvmptss2  5757  fvmptssdm  5767  fprg  5872  dff1o6  5955  tposeq  6491  el2oss1o  6689  nntri1  6742  nntri2or2  6744  nnsseleq  6747  infnninf  7428  infnninfOLD  7429  nninfwlpoimlemg  7479  exmidontri2or  7566  frec2uzf1od  10792  hashinfuni  11165  setsresg  13334  setsslid  13347  strle1g  13403  cncnpi  15219  hmeores  15306  limcimolemlt  15655  recnprss  15678  plycoeid3  15748  0nninf  16908  nninfall  16913