Theorem sseqtrd 3262

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrd.1	|- ( ph -> A C_ B )
sseqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
sseqtrd	|- ( ph -> A C_ C )

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 |- ( ph -> A C_ B )
2		sseqtrd.2	. . 3 |- ( ph -> B = C )
3	2	sseq2d 3254	. 2 |- ( ph -> ( A C_ B <-> A C_ C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1395   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseqtrrd  3263  fssdmd  5487  resasplitss  5507  nnaword2  6668  erssxp  6711  phpm  7035  nninfninc  7301  nnnninfeq  7306  ioodisj  10201  subsubm  13532  subsubg  13750  trivsubgd  13753  trivnsgd  13770  subsubrng  14194  subrgugrp  14220  subsubrg  14225  islssmd  14339  lspun  14382  lspssp  14383  lsslsp  14409  tgcl  14754  basgen  14770  bastop1  14773  bastop2  14774  clsss2  14819  topssnei  14852  cnntr  14915  txbasval  14957  neitx  14958  cnmpt1res  14986  cnmpt2res  14987  imasnopn  14989  hmeontr  15003  tgioo  15244  reldvg  15369  dvfvalap  15371  dvbss  15375  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvcj  15399  vtxdumgrfival  16058