Theorem sseqtrrd 3265

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

Hypotheses

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

Assertion

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

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 |- ( ph -> A C_ B )
2		sseqtrrd.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2236	. 2 |- ( ph -> B = C )
4	1, 3	sseqtrd 3264	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1397   C_ 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:  sseqtrrid  3277  fnfvima  5894  tfrlemiubacc  6501  tfr1onlemubacc  6517  tfrcllemubacc  6530  rdgivallem  6552  nnnninf  7330  nninfwlpoimlemg  7379  ccatass  11194  swrdval2  11241  dfphi2  12815  ctinf  13074  imasaddfnlemg  13420  imasaddvallemg  13421  subsubm  13589  subsubg  13807  subsubrng  14252  subsubrg  14283  lidlss  14514  toponss  14779  ssntr  14875  iscnp3  14956  cnprcl2k  14959  tgcn  14961  tgcnp  14962  ssidcn  14963  cncnp  14983  txcnp  15024  imasnopn  15052  hmeontr  15066  blssec  15191  blssopn  15238  xmettx  15263  metcnp  15265  plyaddlem1  15500  plymullem1  15501  plycoeid3  15510  nnsf  16670  nninfsellemsuc  16677