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  6548  tapeq2  7471  fzowrddc  11227  swrdnd  11239  swrd0g  11240  summodclem2  11942  summodc  11943  zsumdc  11944  fsum3cvg3  11956  prodmodclem2  12137  prodmodc  12138  zproddc  12139  ennnfoneleminc  13031  tgval  13344  prdsval  13355  releqgg  13806  eqgex  13807  eqgfval  13808  opprsubgg  14096  unitsubm  14132  subrngpropd  14229  subrgsubm  14247  issubrg3  14260  subrgpropd  14266  lsslss  14394  lsspropdg  14444  islidlm  14492  rspcl  14504  rspssid  14505  isbasisg  14767  tgss3  14801  restbasg  14891  tgrest  14892  restopn2  14906  cnpnei  14942  cnptopresti  14961  txbas  14981  elmopn  15169  neibl  15214  dvfgg  15411  incistruhgr  15940  edgssv2en  16049  wksfval  16172