Theorem sseqtrri 3229

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)

Hypotheses

Ref	Expression
sseqtrri.1	⊢ 𝐴 ⊆ 𝐵
sseqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
sseqtrri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtrri

Step	Hyp	Ref	Expression
1		sseqtrri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2210	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 3228	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1373   ⊆ wss 3167

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 3173  df-ss 3180

This theorem is referenced by:  eqimss2i  3251  difdif2ss  3431  snsspr1  3783  snsspr2  3784  snsstp1  3785  snsstp2  3786  snsstp3  3787  prsstp12  3788  prsstp13  3789  prsstp23  3790  iunxdif2  3978  pwpwssunieq  4018  sssucid  4466  opabssxp  4753  dmresi  5019  cnvimass  5050  ssrnres  5130  cnvcnv  5140  cnvssrndm  5209  dmmpossx  6292  tfrcllemssrecs  6445  sucinc  6538  mapex  6748  exmidpw  7012  exmidpweq  7013  casefun  7194  djufun  7213  pw1ne1  7348  ressxr  8123  ltrelxr  8140  nnssnn0  9305  un0addcl  9335  un0mulcl  9336  nn0ssxnn0  9368  fzssnn  10197  fzossnn0  10306  isumclim3  11778  isprm3  12484  phimullem  12591  tgvalex  13139  eqgfval  13602  cnfldbas  14366  mpocnfldadd  14367  mpocnfldmul  14369  cnfldcj  14371  cnfldtset  14372  cnfldle  14373  cnfldds  14374  cnrest2  14752  qtopbasss  15037  tgqioo  15071