Theorem eqimss 3278

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

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqimss2  3279  uneqin  3455  ssprsseq  3830  sssnr  3831  sssnm  3832  ssprr  3834  sstpr  3835  snsspw  3842  pwpwssunieq  4054  elpwuni  4055  disjeq2  4063  disjeq1  4066  pwne  4244  pwssunim  4375  poeq2  4391  seeq1  4430  seeq2  4431  trsucss  4514  onsucelsucr  4600  xp11m  5167  funeq  5338  fnresdm  5432  fssxp  5493  ffdm  5496  fcoi1  5508  fof  5550  dff1o2  5579  fvmptss2  5711  fvmptssdm  5721  fprg  5826  dff1o6  5906  tposeq  6399  el2oss1o  6597  nntri1  6650  nntri2or2  6652  nnsseleq  6655  infnninf  7302  infnninfOLD  7303  nninfwlpoimlemg  7353  exmidontri2or  7439  frec2uzf1od  10640  hashinfuni  11011  setsresg  13085  setsslid  13098  strle1g  13154  cncnpi  14917  hmeores  15004  limcimolemlt  15353  recnprss  15376  plycoeid3  15446  0nninf  16430  nninfall  16435