Theorem sseqtrd 2149

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
sseqtrd.1	⊢ (φ → A ⊆ B)
sseqtrd.2	⊢ (φ → B = C)

Assertion

Ref	Expression
sseqtrd	⊢ (φ → A ⊆ C)

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 ⊢ (φ → A ⊆ B)
2		sseqtrd.2	. . 3 ⊢ (φ → B = C)
3	2	sseq2d 2141	. 2 ⊢ (φ → (A ⊆ B ↔ A ⊆ C))
4	1, 3	mpbid 193	1 ⊢ (φ → A ⊆ C)

Syntax hints:   → wi 3   = wceq 992   ⊆ wss 2099

This theorem is referenced by:  sseqtr4d 2150  fconst4 3965  fparlem3 4201  fparlem4 4202  nnaword2 4385  unifi 4701  r1val1 4804  rankr1id 4843  fodom 4944  tgcl 7836  tgss2 7849  2basgen 7853  bastop2 7855  clsss2 7913  iscncl 7980  cnconst 7990  dnsconst 7998  unirnbl 8085  metelcls 8176  bnsscmcl 8785  shsub2 9565  ococin 9573  spanssoc 9595  shub2 9629  chub2 9707  spanpr 9779  ssmd1 10519  mdslj1i 10527  mdslj2i 10528  mdslmd3i 10540  mdexchi 10543  irredlem1 10599  atcvat3i 10605  atcvat4i 10606  mdsymlem1 10612  mdsymlem5 10616  fictblem 11422  finsschain 11425  opnregcld 11467  cncls 11473  cnntr 11474  cptclsscpt 11489  uncomp 11490  compfipin0lem 11492  alexsublem3 11498  alexsublem4 11499  subtopmetlem 11505  reconnlem1 11507  2ndcsb 11537  2ndcctbss 11539  topfneec 11562  fnessref 11564  topjoin 11588  isnrm2 11613  filssufillem 11655  ufinffr 11663  elfilmap3 11692  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  fcluscf 11724  flimfnfcls 11727  fcluscomplem 11732  tailmap 11759  filnetlem5 11767  fzm1 11867  cnimass 11949  cnss 11953  paste 11954  hmeocld 11961

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain