Theorem sseq1d 3277

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 3271	. 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 1402   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12d  3279  eqsstrd  3284  snssgOLD  3846  ssiun2s  4051  treq  4230  onsucsssucexmid  4669  funimass1  5453  feq1  5511  sbcfg  5527  fvmptssdm  5784  fvimacnvi  5814  nnsucsssuc  6755  ereq1  6804  elpm2r  6930  fipwssg  7303  nnnninf  7456  ctssexmid  7480  rspssp  14803  iscnp  15223  iscnp4  15242  cnntr  15249  cnconst2  15257  cnptopresti  15262  cnptoprest  15263  txbas  15282  txcnp  15295  txdis  15301  txdis1cn  15302  blssps  15451  blss  15452  ssblex  15455  blin2  15456  metss2  15522  metrest  15530  metcnp3  15535  cnopnap  15635  limccl  15683  ellimc3apf  15684  ausgrumgrien  16325  ausgrusgrien  16326  eupth2lem3lem4fi  16628