Theorem sseqtrrd 3266

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 2237	. 2 |- ( ph -> B = C )
4	1, 3	sseqtrd 3265	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1397   C_ wss 3200

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sseqtrrid  3278  fnfvima  5888  tfrlemiubacc  6495  tfr1onlemubacc  6511  tfrcllemubacc  6524  rdgivallem  6546  nnnninf  7324  nninfwlpoimlemg  7373  ccatass  11184  swrdval2  11231  dfphi2  12791  ctinf  13050  imasaddfnlemg  13396  imasaddvallemg  13397  subsubm  13565  subsubg  13783  subsubrng  14227  subsubrg  14258  lidlss  14489  toponss  14749  ssntr  14845  iscnp3  14926  cnprcl2k  14929  tgcn  14931  tgcnp  14932  ssidcn  14933  cncnp  14953  txcnp  14994  imasnopn  15022  hmeontr  15036  blssec  15161  blssopn  15208  xmettx  15233  metcnp  15235  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  nnsf  16607  nninfsellemsuc  16614