Theorem eqsstrd 3184

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

Hypotheses

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

Assertion

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

Proof of Theorem eqsstrd

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 |- ( ph -> B C_ C )
2		eqsstrd.1	. . 3 |- ( ph -> A = B )
3	2	sseq1d 3177	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
4	1, 3	mpbird 166	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1349   C_ wss 3122

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 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-11 1500  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-in 3128  df-ss 3135

This theorem is referenced by:  eqsstrrd  3185  eqsstrdi  3200  tfisi  4572  funresdfunsnss  5703  suppssof1  6082  phplem4dom  6844  fival  6951  fiuni  6959  cardonle  7168  exmidfodomrlemim  7182  frecuzrdgtclt  10381  ennnfonelemkh  12371  ennnfonelemf1  12377  strfvssn  12442  setscom  12460  tgrest  13048  resttopon  13050  rest0  13058  lmtopcnp  13129  metequiv2  13375  xmettx  13389  ellimc3apf  13508  dvfvalap  13529  dvcjbr  13551  dvcj  13552  dvfre  13553  nnsf  14123