Theorem eqimss 3292

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

Syntax hints:   → wi 4   = wceq 1398   ⊆ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  eqimss2  3293  uneqin  3472  ssprsseq  3856  sssnr  3857  sssnm  3858  ssprr  3860  sstpr  3861  snsspw  3868  pwpwssunieq  4080  elpwuni  4081  disjeq2  4089  disjeq1  4092  pwne  4273  pwssunim  4405  poeq2  4421  seeq1  4460  seeq2  4461  trsucss  4544  onsucelsucr  4630  xp11m  5201  funeq  5372  fnresdm  5467  fssxp  5530  ffdm  5533  fcoi1  5547  fof  5590  dff1o2  5619  fvmptss2  5752  fvmptssdm  5762  fprg  5867  dff1o6  5949  tposeq  6478  el2oss1o  6676  nntri1  6729  nntri2or2  6731  nnsseleq  6734  infnninf  7415  infnninfOLD  7416  nninfwlpoimlemg  7466  exmidontri2or  7553  frec2uzf1od  10768  hashinfuni  11140  setsresg  13250  setsslid  13263  strle1g  13319  cncnpi  15093  hmeores  15180  limcimolemlt  15529  recnprss  15552  plycoeid3  15622  0nninf  16782  nninfall  16787