Theorem sseq1d 3257

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 3251	. 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 105   = wceq 1398   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12d  3259  eqsstrd  3264  snssgOLD  3814  ssiun2s  4019  treq  4198  onsucsssucexmid  4631  funimass1  5414  feq1  5472  sbcfg  5488  fvmptssdm  5740  fvimacnvi  5770  nnsucsssuc  6703  ereq1  6752  elpm2r  6878  fipwssg  7221  nnnninf  7368  ctssexmid  7392  rspssp  14573  iscnp  14993  iscnp4  15012  cnntr  15019  cnconst2  15027  cnptopresti  15032  cnptoprest  15033  txbas  15052  txcnp  15065  txdis  15071  txdis1cn  15072  blssps  15221  blss  15222  ssblex  15225  blin2  15226  metss2  15292  metrest  15300  metcnp3  15305  cnopnap  15405  limccl  15453  ellimc3apf  15454  ausgrumgrien  16094  ausgrusgrien  16095  eupth2lem3lem4fi  16397