Theorem sseqtr 1532

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
sseqtr.1	⊢ A ⊆ B
sseqtr.2	⊢ B = C

Assertion

Ref	Expression
sseqtr	⊢ A ⊆ C

Proof of Theorem sseqtr

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2 ⊢ A ⊆ B
2		sseqtr.2	. . 3 ⊢ B = C
3	2	sseq2i 1525	. 2 ⊢ (A ⊆ B ↔ A ⊆ C)
4	1, 3	mpbi 164	1 ⊢ A ⊆ C

Syntax hints:   = wceq 1091   ⊆ wss 1487

This theorem is referenced by:  sseqtr4 1533  ssab 1555  ssun2 1622  uni0 1938  opabss 2100  dmexg 2551  rnexg 2569  ecopoprdm 3245  sbthlem7 3355  cf0 3705  cfsuc 3709  cfom 3710  choc1 5292  shlej1 5349  shslub 5359  chub2 5391  span0 5448  spanun 5450  sshhococ 5451  chsup0 5453  spansnpj 5481  pj3 5660  hatomistic 5755  atcvat4 5775

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org