Theorem sseq2d 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
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 3248	. 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 1395   C_ wss 3197

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 3203  df-ss 3210

This theorem is referenced by:  sseq12d  3255  sseqtrd  3262  exmidsssn  4286  exmidsssnc  4287  onsucsssucexmid  4619  sbcrel  4805  funimass2  5399  fnco  5431  fnssresb  5435  fnimaeq0  5445  foimacnv  5592  fvelimab  5692  ssimaexg  5698  fvmptss2  5711  rdgss  6535  tapeq2  7450  fzowrddc  11194  swrdnd  11206  swrd0g  11207  summodclem2  11908  summodc  11909  zsumdc  11910  fsum3cvg3  11922  prodmodclem2  12103  prodmodc  12104  zproddc  12105  ennnfoneleminc  12997  tgval  13310  prdsval  13321  releqgg  13772  eqgex  13773  eqgfval  13774  opprsubgg  14062  unitsubm  14098  subrngpropd  14195  subrgsubm  14213  issubrg3  14226  subrgpropd  14232  lsslss  14360  lsspropdg  14410  islidlm  14458  rspcl  14470  rspssid  14471  isbasisg  14733  tgss3  14767  restbasg  14857  tgrest  14858  restopn2  14872  cnpnei  14908  cnptopresti  14927  txbas  14947  elmopn  15135  neibl  15180  dvfgg  15377  incistruhgr  15905  edgssv2en  16012  wksfval  16063