Theorem eqimss 2974

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

Assertion

Ref	Expression
eqimss	⊢ (A = B → A ⊆ B)

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 2937	. 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
2	1	simplbi 259	1 ⊢ (A = B → A ⊆ B)

Syntax hints:   → wi 4   = wceq 1228   ⊆ wss 2894

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908

This theorem is referenced by:  eqimss2  2975  sspssr  3020  sspsstrir  3023  uneqin  3165  sssnr  3498  sssnm  3499  ssprr  3501  sstpr  3502  snsspw  3509  elpwuni  3715  disjeq2  3723  disjeq1  3726  pwne  3887  pwssunim  3995  poeq2  4011  seeq1  4044  seeq2  4045  trsucss  4110  onsucelsucr  4183  xp11m  4686  funeq  4847  fnresdm  4934  fssxp  4983  ffdm  4986  fcoi1  4995  fof  5031  dff1o2  5056  fvmptss2  5172  fvmptssdm  5180  fprg  5271  dff1o6  5341  tposeq  5784  nntri1  5989