Theorem sseqtrri 3214

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

Syntax hints:   = wceq 1364   ⊆ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  eqimss2i  3236  difdif2ss  3416  snsspr1  3766  snsspr2  3767  snsstp1  3768  snsstp2  3769  snsstp3  3770  prsstp12  3771  prsstp13  3772  prsstp23  3773  iunxdif2  3961  pwpwssunieq  4001  sssucid  4446  opabssxp  4733  dmresi  4997  cnvimass  5028  ssrnres  5108  cnvcnv  5118  cnvssrndm  5187  dmmpossx  6252  tfrcllemssrecs  6405  sucinc  6498  mapex  6708  exmidpw  6964  exmidpweq  6965  casefun  7144  djufun  7163  pw1ne1  7289  ressxr  8063  ltrelxr  8080  nnssnn0  9243  un0addcl  9273  un0mulcl  9274  nn0ssxnn0  9306  fzssnn  10134  fzossnn0  10242  isumclim3  11566  isprm3  12256  phimullem  12363  tgvalex  12874  eqgfval  13292  cnfldbas  14051  cnfldadd  14052  cnfldmul  14054  cnfldcj  14056  cnrest2  14404  qtopbasss  14689  tgqioo  14715