Theorem sseqtrri 3283

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 2242	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 3282	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1402   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  eqimss2i  3305  difdif2ss  3488  snsspr1  3861  snsspr2  3862  snsstp1  3863  snsstp2  3864  snsstp3  3865  prsstp12  3866  prsstp13  3867  prsstp23  3868  iunxdif2  4059  pwpwssunieq  4099  sssucid  4558  opabssxp  4847  dmresi  5116  cnvimass  5148  ssrnres  5228  cnvcnv  5238  cnvssrndm  5307  dmmpossx  6429  tfrcllemssrecs  6617  sucinc  6712  mapex  6922  exmidpw  7209  exmidpweq  7210  casefun  7419  djufun  7438  pw1ne1  7582  ressxr  8363  ltrelxr  8380  nnssnn0  9549  un0addcl  9579  un0mulcl  9580  nn0ssxnn0  9616  fzssnn  10457  fzossnn0  10567  isumclim3  12173  isprm3  12879  phimullem  12986  ballotfilem7  13262  tgvalex  13600  eqgfval  14008  cnfldbas  14880  mpocnfldadd  14881  mpocnfldmul  14883  cnfldcj  14885  cnfldtset  14886  cnfldle  14887  cnfldds  14888  cnrest2  15320  qtopbasss  15605  tgqioo  15639