Theorem sseqtrri 3262

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

Syntax hints:   = wceq 1397   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqimss2i  3284  difdif2ss  3464  snsspr1  3821  snsspr2  3822  snsstp1  3823  snsstp2  3824  snsstp3  3825  prsstp12  3826  prsstp13  3827  prsstp23  3828  iunxdif2  4019  pwpwssunieq  4059  sssucid  4512  opabssxp  4800  dmresi  5068  cnvimass  5099  ssrnres  5179  cnvcnv  5189  cnvssrndm  5258  dmmpossx  6364  tfrcllemssrecs  6518  sucinc  6613  mapex  6823  exmidpw  7100  exmidpweq  7101  casefun  7284  djufun  7303  pw1ne1  7447  ressxr  8223  ltrelxr  8240  nnssnn0  9405  un0addcl  9435  un0mulcl  9436  nn0ssxnn0  9468  fzssnn  10303  fzossnn0  10412  isumclim3  11986  isprm3  12692  phimullem  12799  tgvalex  13348  eqgfval  13811  cnfldbas  14577  mpocnfldadd  14578  mpocnfldmul  14580  cnfldcj  14582  cnfldtset  14583  cnfldle  14584  cnfldds  14585  cnrest2  14963  qtopbasss  15248  tgqioo  15282