Theorem eqimss 3246

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

Syntax hints:   → wi 4   = wceq 1372   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  eqimss2  3247  uneqin  3423  sssnr  3793  sssnm  3794  ssprr  3796  sstpr  3797  snsspw  3804  pwpwssunieq  4015  elpwuni  4016  disjeq2  4024  disjeq1  4027  pwne  4203  pwssunim  4329  poeq2  4345  seeq1  4384  seeq2  4385  trsucss  4468  onsucelsucr  4554  xp11m  5118  funeq  5288  fnresdm  5379  fssxp  5437  ffdm  5440  fcoi1  5450  fof  5492  dff1o2  5521  fvmptss2  5648  fvmptssdm  5658  fprg  5757  dff1o6  5835  tposeq  6323  el2oss1o  6519  nntri1  6572  nntri2or2  6574  nnsseleq  6577  infnninf  7208  infnninfOLD  7209  nninfwlpoimlemg  7259  exmidontri2or  7337  frec2uzf1od  10532  hashinfuni  10903  setsresg  12789  setsslid  12802  strle1g  12857  cncnpi  14618  hmeores  14705  limcimolemlt  15054  recnprss  15077  plycoeid3  15147  0nninf  15805  nninfall  15810