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  3829  sssnr  3830  sssnm  3831  ssprr  3833  sstpr  3834  snsspw  3841  pwpwssunieq  4053  elpwuni  4054  disjeq2  4062  disjeq1  4065  pwne  4243  pwssunim  4374  poeq2  4390  seeq1  4429  seeq2  4430  trsucss  4513  onsucelsucr  4599  xp11m  5166  funeq  5337  fnresdm  5431  fssxp  5490  ffdm  5493  fcoi1  5505  fof  5547  dff1o2  5576  fvmptss2  5708  fvmptssdm  5718  fprg  5821  dff1o6  5899  tposeq  6391  el2oss1o  6587  nntri1  6640  nntri2or2  6642  nnsseleq  6645  infnninf  7287  infnninfOLD  7288  nninfwlpoimlemg  7338  exmidontri2or  7424  frec2uzf1od  10623  hashinfuni  10994  setsresg  13065  setsslid  13078  strle1g  13134  cncnpi  14896  hmeores  14983  limcimolemlt  15332  recnprss  15355  plycoeid3  15425  0nninf  16329  nninfall  16334