Theorem sseqtr4 1533

Description: Substitution of equality into a subclass relationship.

Hypotheses

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

Assertion

Ref	Expression
sseqtr4	⊢ A ⊆ C

Proof of Theorem sseqtr4

Step	Hyp	Ref	Expression
1		sseqtr4.1	. 2 ⊢ A ⊆ B
2		sseqtr4.2	. . 3 ⊢ C = B
3	2	cleqcomi 1105	. 2 ⊢ B = C
4	1, 3	sseqtr 1532	1 ⊢ A ⊆ C

Syntax hints:   = wceq 1091   ⊆ wss 1487

This theorem is referenced by:  sssucid 2300  opabssxp 2468  relopab 2494  dmresi 2600  cnvcnv 2661  fnresi 2737  fvclss 2907  tfrlem11 2959  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  oawordeulem 3156  mapex 3261  trcl 3489  rankpw 3528  aceq3lem 3555  aceq3 3556  cfsuc 3709  cfom 3710  nnssnn0 4537  shsspwh 5153  shlesb1 5360  sshhococ 5451  pjoml5 5498  osumlem8 5537  pjclem1 5649  pjc 5654

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