Theorem sseqtrrd 3186

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

Syntax hints:   -> wi 4   = wceq 1348   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sseqtrrid  3198  fnfvima  5730  tfrlemiubacc  6309  tfr1onlemubacc  6325  tfrcllemubacc  6338  rdgivallem  6360  nnnninf  7102  nninfwlpoimlemg  7151  dfphi2  12174  ctinf  12385  toponss  12818  ssntr  12916  iscnp3  12997  cnprcl2k  13000  tgcn  13002  tgcnp  13003  ssidcn  13004  cncnp  13024  txcnp  13065  imasnopn  13093  hmeontr  13107  blssec  13232  blssopn  13279  xmettx  13304  metcnp  13306  nnsf  14038  nninfsellemsuc  14045