Theorem sseqtrri 3190

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

Syntax hints:   = wceq 1353   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  eqimss2i  3212  difdif2ss  3392  snsspr1  3740  snsspr2  3741  snsstp1  3742  snsstp2  3743  snsstp3  3744  prsstp12  3745  prsstp13  3746  prsstp23  3747  iunxdif2  3933  pwpwssunieq  3973  sssucid  4413  opabssxp  4698  dmresi  4959  cnvimass  4988  ssrnres  5068  cnvcnv  5078  cnvssrndm  5147  dmmpossx  6195  tfrcllemssrecs  6348  sucinc  6441  mapex  6649  exmidpw  6903  exmidpweq  6904  casefun  7079  djufun  7098  pw1ne1  7223  ressxr  7995  ltrelxr  8012  nnssnn0  9173  un0addcl  9203  un0mulcl  9204  nn0ssxnn0  9236  fzssnn  10061  fzossnn0  10168  isumclim3  11422  isprm3  12108  phimullem  12215  cnfldbas  13264  cnfldadd  13265  cnfldmul  13266  cnfldcj  13267  tgvalex  13332  cnrest2  13518  qtopbasss  13803  tgqioo  13829