Theorem sseqtrri 3236

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

Syntax hints:   = wceq 1373   ⊆ wss 3174

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 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  eqimss2i  3258  difdif2ss  3438  snsspr1  3792  snsspr2  3793  snsstp1  3794  snsstp2  3795  snsstp3  3796  prsstp12  3797  prsstp13  3798  prsstp23  3799  iunxdif2  3990  pwpwssunieq  4030  sssucid  4480  opabssxp  4767  dmresi  5033  cnvimass  5064  ssrnres  5144  cnvcnv  5154  cnvssrndm  5223  dmmpossx  6308  tfrcllemssrecs  6461  sucinc  6554  mapex  6764  exmidpw  7031  exmidpweq  7032  casefun  7213  djufun  7232  pw1ne1  7375  ressxr  8151  ltrelxr  8168  nnssnn0  9333  un0addcl  9363  un0mulcl  9364  nn0ssxnn0  9396  fzssnn  10225  fzossnn0  10334  isumclim3  11849  isprm3  12555  phimullem  12662  tgvalex  13210  eqgfval  13673  cnfldbas  14437  mpocnfldadd  14438  mpocnfldmul  14440  cnfldcj  14442  cnfldtset  14443  cnfldle  14444  cnfldds  14445  cnrest2  14823  qtopbasss  15108  tgqioo  15142