Theorem eqimss 3093

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

Syntax hints:   → wi 4   = wceq 1296   ⊆ wss 3013

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026

This theorem is referenced by:  eqimss2  3094  uneqin  3266  sssnr  3619  sssnm  3620  ssprr  3622  sstpr  3623  snsspw  3630  pwpwssunieq  3839  elpwuni  3840  disjeq2  3848  disjeq1  3851  pwne  4016  pwssunim  4135  poeq2  4151  seeq1  4190  seeq2  4191  trsucss  4274  onsucelsucr  4353  xp11m  4903  funeq  5069  fnresdm  5157  fssxp  5213  ffdm  5216  fcoi1  5226  fof  5268  dff1o2  5293  fvmptss2  5414  fvmptssdm  5423  fprg  5519  dff1o6  5593  tposeq  6050  nntri1  6297  nntri2or2  6299  nnsseleq  6302  infnninf  6893  frec2uzf1od  9962  hashinfuni  10316  setsresg  11697  setsslid  11709  strle1g  11749  cncnpi  12095  el2oss1o  12609  0nninf  12614  nninfall  12621