Theorem sseqtrri 3261

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

Syntax hints:   = wceq 1397   ⊆ wss 3199

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 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  eqimss2i  3283  difdif2ss  3463  snsspr1  3822  snsspr2  3823  snsstp1  3824  snsstp2  3825  snsstp3  3826  prsstp12  3827  prsstp13  3828  prsstp23  3829  iunxdif2  4020  pwpwssunieq  4060  sssucid  4514  opabssxp  4802  dmresi  5070  cnvimass  5101  ssrnres  5181  cnvcnv  5191  cnvssrndm  5260  dmmpossx  6369  tfrcllemssrecs  6523  sucinc  6618  mapex  6828  exmidpw  7105  exmidpweq  7106  casefun  7289  djufun  7308  pw1ne1  7452  ressxr  8228  ltrelxr  8245  nnssnn0  9410  un0addcl  9440  un0mulcl  9441  nn0ssxnn0  9473  fzssnn  10308  fzossnn0  10417  isumclim3  12007  isprm3  12713  phimullem  12820  tgvalex  13369  eqgfval  13832  cnfldbas  14598  mpocnfldadd  14599  mpocnfldmul  14601  cnfldcj  14603  cnfldtset  14604  cnfldle  14605  cnfldds  14606  cnrest2  14989  qtopbasss  15274  tgqioo  15308