Theorem eqimss 3251

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

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  eqimss2  3252  uneqin  3428  sssnr  3800  sssnm  3801  ssprr  3803  sstpr  3804  snsspw  3811  pwpwssunieq  4022  elpwuni  4023  disjeq2  4031  disjeq1  4034  pwne  4212  pwssunim  4339  poeq2  4355  seeq1  4394  seeq2  4395  trsucss  4478  onsucelsucr  4564  xp11m  5130  funeq  5300  fnresdm  5394  fssxp  5453  ffdm  5456  fcoi1  5468  fof  5510  dff1o2  5539  fvmptss2  5667  fvmptssdm  5677  fprg  5780  dff1o6  5858  tposeq  6346  el2oss1o  6542  nntri1  6595  nntri2or2  6597  nnsseleq  6600  infnninf  7241  infnninfOLD  7242  nninfwlpoimlemg  7292  exmidontri2or  7374  frec2uzf1od  10573  hashinfuni  10944  setsresg  12945  setsslid  12958  strle1g  13013  cncnpi  14775  hmeores  14862  limcimolemlt  15211  recnprss  15234  plycoeid3  15304  0nninf  16082  nninfall  16087