Theorem sseqtrri 3182

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

Syntax hints:   = wceq 1348   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqimss2i  3204  difdif2ss  3384  snsspr1  3726  snsspr2  3727  snsstp1  3728  snsstp2  3729  snsstp3  3730  prsstp12  3731  prsstp13  3732  prsstp23  3733  iunxdif2  3919  pwpwssunieq  3959  sssucid  4398  opabssxp  4683  dmresi  4944  cnvimass  4972  ssrnres  5051  cnvcnv  5061  cnvssrndm  5130  dmmpossx  6176  tfrcllemssrecs  6329  sucinc  6422  mapex  6629  exmidpw  6883  exmidpweq  6884  casefun  7059  djufun  7078  pw1ne1  7195  ressxr  7952  ltrelxr  7969  nnssnn0  9127  un0addcl  9157  un0mulcl  9158  nn0ssxnn0  9190  fzssnn  10013  fzossnn0  10120  isumclim3  11375  isprm3  12061  phimullem  12168  tgvalex  12805  cnrest2  12991  qtopbasss  13276  tgqioo  13302