Theorem sseq1d 3254

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 3248	. 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 1395   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sseq12d  3256  eqsstrd  3261  snssgOLD  3807  ssiun2s  4012  treq  4191  onsucsssucexmid  4623  funimass1  5404  feq1  5462  sbcfg  5478  fvmptssdm  5727  fvimacnvi  5757  nnsucsssuc  6655  ereq1  6704  elpm2r  6830  fipwssg  7169  nnnninf  7316  ctssexmid  7340  rspssp  14498  iscnp  14913  iscnp4  14932  cnntr  14939  cnconst2  14947  cnptopresti  14952  cnptoprest  14953  txbas  14972  txcnp  14985  txdis  14991  txdis1cn  14992  blssps  15141  blss  15142  ssblex  15145  blin2  15146  metss2  15212  metrest  15220  metcnp3  15225  cnopnap  15325  limccl  15373  ellimc3apf  15374  ausgrumgrien  16009  ausgrusgrien  16010