Theorem sseq1d 3176

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 3170	. 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 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:  sseq12d  3178  eqsstrd  3183  snssg  3716  ssiun2s  3917  treq  4093  onsucsssucexmid  4511  funimass1  5275  feq1  5330  sbcfg  5346  fvmptssdm  5580  fvimacnvi  5610  nnsucsssuc  6471  ereq1  6520  elpm2r  6644  fipwssg  6956  nnnninf  7102  ctssexmid  7126  iscnp  12993  iscnp4  13012  cnntr  13019  cnconst2  13027  cnptopresti  13032  cnptoprest  13033  txbas  13052  txcnp  13065  txdis  13071  txdis1cn  13072  blssps  13221  blss  13222  ssblex  13225  blin2  13226  metss2  13292  metrest  13300  metcnp3  13305  cnopnap  13388  limccl  13422  ellimc3apf  13423