Theorem eqsstrrd 3230

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

Hypotheses

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

Assertion

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

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 |- ( ph -> B = A )
2	1	eqcomd 2211	. 2 |- ( ph -> A = B )
3		eqsstrrd.2	. 2 |- ( ph -> B C_ C )
4	2, 3	eqsstrd 3229	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  ssxpbm  5119  ssxp1  5120  ssxp2  5121  suppssof1  6178  tfrlemiubacc  6418  tfr1onlemubacc  6434  tfrcllemubacc  6447  oaword1  6559  phplem4dom  6961  fisseneq  7033  nnnninfeq2  7233  archnqq  7532  hashdmprop2dom  10991  imasaddfnlemg  13179  resmhm2  13353  ringidss  13824  subrg1  14026  subrgdvds  14030  subrguss  14031  subrginv  14032  islss3  14174  lspsnneg  14215  epttop  14595  metequiv2  15001  limccnpcntop  15180  limccnp2lem  15181  limccnp2cntop  15182  nnsf  15979