Theorem sseq1d 3209

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 3203	. 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 1364   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sseq12d  3211  eqsstrd  3216  snssgOLD  3755  ssiun2s  3957  treq  4134  onsucsssucexmid  4560  funimass1  5332  feq1  5387  sbcfg  5403  fvmptssdm  5643  fvimacnvi  5673  nnsucsssuc  6547  ereq1  6596  elpm2r  6722  fipwssg  7040  nnnninf  7187  ctssexmid  7211  rspssp  13993  iscnp  14378  iscnp4  14397  cnntr  14404  cnconst2  14412  cnptopresti  14417  cnptoprest  14418  txbas  14437  txcnp  14450  txdis  14456  txdis1cn  14457  blssps  14606  blss  14607  ssblex  14610  blin2  14611  metss2  14677  metrest  14685  metcnp3  14690  cnopnap  14790  limccl  14838  ellimc3apf  14839