Theorem sseq2d 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
sseq2d	|- ( ph -> ( C C_ A <-> C C_ B ) )

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- ( ph -> A = B )
2		sseq2 3251	. 2 |- ( A = B -> ( C C_ A <-> C C_ B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C C_ A <-> C C_ B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sseq12d  3258  sseqtrd  3265  exmidsssn  4292  exmidsssnc  4293  onsucsssucexmid  4625  sbcrel  4812  funimass2  5408  fnco  5440  fnssresb  5444  fnimaeq0  5454  foimacnv  5601  fvelimab  5702  ssimaexg  5708  fvmptss2  5721  rdgss  6549  tapeq2  7472  fzowrddc  11232  swrdnd  11244  swrd0g  11245  summodclem2  11961  summodc  11962  zsumdc  11963  fsum3cvg3  11975  prodmodclem2  12156  prodmodc  12157  zproddc  12158  ennnfoneleminc  13050  tgval  13363  prdsval  13374  releqgg  13825  eqgex  13826  eqgfval  13827  opprsubgg  14116  unitsubm  14152  subrngpropd  14249  subrgsubm  14267  issubrg3  14280  subrgpropd  14286  lsslss  14414  lsspropdg  14464  islidlm  14512  rspcl  14524  rspssid  14525  isbasisg  14787  tgss3  14821  restbasg  14911  tgrest  14912  restopn2  14926  cnpnei  14962  cnptopresti  14981  txbas  15001  elmopn  15189  neibl  15234  dvfgg  15431  incistruhgr  15960  edgssv2en  16069  wksfval  16192