Theorem sseqtrrd 3219

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

Syntax hints:   -> wi 4   = wceq 1364   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sseqtrrid  3231  fnfvima  5794  tfrlemiubacc  6385  tfr1onlemubacc  6401  tfrcllemubacc  6414  rdgivallem  6436  nnnninf  7187  nninfwlpoimlemg  7236  dfphi2  12361  ctinf  12590  imasaddfnlemg  12900  imasaddvallemg  12901  subsubm  13058  subsubg  13270  subsubrng  13713  subsubrg  13744  lidlss  13975  toponss  14205  ssntr  14301  iscnp3  14382  cnprcl2k  14385  tgcn  14387  tgcnp  14388  ssidcn  14389  cncnp  14409  txcnp  14450  imasnopn  14478  hmeontr  14492  blssec  14617  blssopn  14664  xmettx  14689  metcnp  14691  plyaddlem1  14926  plymullem1  14927  nnsf  15565  nninfsellemsuc  15572