Theorem eqimss 3211

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

Syntax hints:   → wi 4   = wceq 1353   ⊆ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  eqimss2  3212  uneqin  3388  sssnr  3755  sssnm  3756  ssprr  3758  sstpr  3759  snsspw  3766  pwpwssunieq  3977  elpwuni  3978  disjeq2  3986  disjeq1  3989  pwne  4162  pwssunim  4286  poeq2  4302  seeq1  4341  seeq2  4342  trsucss  4425  onsucelsucr  4509  xp11m  5069  funeq  5238  fnresdm  5327  fssxp  5385  ffdm  5388  fcoi1  5398  fof  5440  dff1o2  5468  fvmptss2  5594  fvmptssdm  5603  fprg  5702  dff1o6  5780  tposeq  6251  el2oss1o  6447  nntri1  6500  nntri2or2  6502  nnsseleq  6505  infnninf  7125  infnninfOLD  7126  nninfwlpoimlemg  7176  exmidontri2or  7245  frec2uzf1od  10409  hashinfuni  10760  setsresg  12503  setsslid  12516  strle1g  12568  cncnpi  13889  hmeores  13976  limcimolemlt  14294  recnprss  14317  0nninf  14915  nninfall  14920