Theorem sseqtri 3260

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)

Hypotheses

Ref	Expression
sseqtr.1	⊢ 𝐴 ⊆ 𝐵
sseqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
sseqtri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtri

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	sseq2i 3253	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	mpbi 145	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:  sseqtrri  3261  eqimssi  3282  abssi  3301  ssun2  3370  inssddif  3447  difdifdirss  3578  ifidss  3622  pwundifss  4384  unixpss  4841  0ima  5098  sbthlem7  7167  0bits  12543  ssnnctlemct  13090  prdsvallem  13378  toponsspwpwg  14775  eltg4i  14808  ntrss2  14874  isopn3  14878  tgioo  15307  dvfvalap  15434  dvcnp2cntop  15452