Theorem sseq2d 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
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 3203	. 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 1364   C_ wss 3153

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 3159  df-ss 3166

This theorem is referenced by:  sseq12d  3210  sseqtrd  3217  exmidsssn  4231  exmidsssnc  4232  onsucsssucexmid  4559  sbcrel  4745  funimass2  5332  fnco  5362  fnssresb  5366  fnimaeq0  5375  foimacnv  5518  fvelimab  5613  ssimaexg  5619  fvmptss2  5632  rdgss  6436  tapeq2  7313  summodclem2  11525  summodc  11526  zsumdc  11527  fsum3cvg3  11539  prodmodclem2  11720  prodmodc  11721  zproddc  11722  ennnfoneleminc  12568  tgval  12873  releqgg  13290  eqgex  13291  eqgfval  13292  opprsubgg  13580  unitsubm  13615  subrngpropd  13712  subrgsubm  13730  issubrg3  13743  subrgpropd  13749  lsslss  13877  lsspropdg  13927  islidlm  13975  rspcl  13987  rspssid  13988  isbasisg  14212  tgss3  14246  restbasg  14336  tgrest  14337  restopn2  14351  cnpnei  14387  cnptopresti  14406  txbas  14426  elmopn  14614  neibl  14659  dvfgg  14842