Theorem sseq1d 3157

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sseq1d	|- ( ph -> ( A C_ C <-> B C_ C ) )

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- ( ph -> A = B )
2		sseq1 3151	. 2 |- ( A = B -> ( A C_ C <-> B C_ C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335   C_ wss 3102

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sseq12d  3159  eqsstrd  3164  snssg  3692  ssiun2s  3893  treq  4068  onsucsssucexmid  4486  funimass1  5247  feq1  5302  sbcfg  5318  fvmptssdm  5552  fvimacnvi  5581  nnsucsssuc  6439  ereq1  6487  elpm2r  6611  fipwssg  6923  nnnninf  7069  ctssexmid  7093  iscnp  12599  iscnp4  12618  cnntr  12625  cnconst2  12633  cnptopresti  12638  cnptoprest  12639  txbas  12658  txcnp  12671  txdis  12677  txdis1cn  12678  blssps  12827  blss  12828  ssblex  12831  blin2  12832  metss2  12898  metrest  12906  metcnp3  12911  cnopnap  12994  limccl  13028  ellimc3apf  13029