Theorem sseq1d 3267

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 3261	. 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 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  sseq12d  3269  eqsstrd  3274  snssgOLD  3830  ssiun2s  4035  treq  4214  onsucsssucexmid  4649  funimass1  5433  feq1  5491  sbcfg  5507  fvmptssdm  5762  fvimacnvi  5792  nnsucsssuc  6725  ereq1  6774  elpm2r  6900  fipwssg  7266  nnnninf  7417  ctssexmid  7441  rspssp  14642  iscnp  15064  iscnp4  15083  cnntr  15090  cnconst2  15098  cnptopresti  15103  cnptoprest  15104  txbas  15123  txcnp  15136  txdis  15142  txdis1cn  15143  blssps  15292  blss  15293  ssblex  15296  blin2  15297  metss2  15363  metrest  15371  metcnp3  15376  cnopnap  15476  limccl  15524  ellimc3apf  15525  ausgrumgrien  16165  ausgrusgrien  16166  eupth2lem3lem4fi  16468