Theorem eqimss 3062

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

Syntax hints:   → wi 4   = wceq 1285   ⊆ wss 2984

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2990  df-ss 2997

This theorem is referenced by:  eqimss2  3063  uneqin  3233  sssnr  3571  sssnm  3572  ssprr  3574  sstpr  3575  snsspw  3582  elpwuni  3788  disjeq2  3796  disjeq1  3799  pwne  3960  pwssunim  4074  poeq2  4090  seeq1  4129  seeq2  4130  trsucss  4213  onsucelsucr  4287  xp11m  4822  funeq  4987  fnresdm  5075  fssxp  5126  ffdm  5129  fcoi1  5138  fof  5180  dff1o2  5205  fvmptss2  5323  fvmptssdm  5331  fprg  5421  dff1o6  5494  tposeq  5943  nntri1  6188  nntri2or2  6190  nnsseleq  6193  infnninf  8643  frec2uzf1od  9701  hashinfuni  10019