Theorem sseqtrri 3239

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

Syntax hints:   = wceq 1375   ⊆ wss 3177

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  eqimss2i  3261  difdif2ss  3441  snsspr1  3795  snsspr2  3796  snsstp1  3797  snsstp2  3798  snsstp3  3799  prsstp12  3800  prsstp13  3801  prsstp23  3802  iunxdif2  3993  pwpwssunieq  4033  sssucid  4483  opabssxp  4770  dmresi  5036  cnvimass  5067  ssrnres  5147  cnvcnv  5157  cnvssrndm  5226  dmmpossx  6315  tfrcllemssrecs  6468  sucinc  6561  mapex  6771  exmidpw  7038  exmidpweq  7039  casefun  7220  djufun  7239  pw1ne1  7382  ressxr  8158  ltrelxr  8175  nnssnn0  9340  un0addcl  9370  un0mulcl  9371  nn0ssxnn0  9403  fzssnn  10232  fzossnn0  10341  isumclim3  11900  isprm3  12606  phimullem  12713  tgvalex  13262  eqgfval  13725  cnfldbas  14489  mpocnfldadd  14490  mpocnfldmul  14492  cnfldcj  14494  cnfldtset  14495  cnfldle  14496  cnfldds  14497  cnrest2  14875  qtopbasss  15160  tgqioo  15194