Theorem sseq2d 3278

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 3272	. 2 |- ( A = B -> ( C C_ A <-> C C_ B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C C_ A <-> C C_ B ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sseq12d  3279  sseqtrd  3286  exmidsssn  4341  exmidsssnc  4342  onsucsssucexmid  4676  sbcrel  4863  funimass2  5462  fnco  5494  fnssresb  5498  fnimaeq0  5508  foimacnv  5660  fvelimab  5762  ssimaexg  5768  fvmptss2  5783  rdgss  6658  papeq2  7616  tapeq2  7625  fzowrddc  11441  swrdnd  11453  swrd0g  11454  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3cvg3  12188  prodmodclem2  12369  prodmodc  12370  zproddc  12371  ennnfoneleminc  13360  tgval  13675  releqgg  14082  eqgex  14083  eqgfval  14084  sscntz  14158  resscntz  14166  prdsval  14280  opprsubgg  14499  unitsubm  14535  subrngpropd  14633  subrgsubm  14651  issubrg3  14664  subrgpropd  14670  lsslss  14827  lsspropdg  14877  islidlm  14925  rspcl  14937  rspssid  14938  isbasisg  15270  tgss3  15304  restbasg  15394  tgrest  15395  restopn2  15409  cnpnei  15445  cnptopresti  15464  txbas  15484  elmopn  15672  neibl  15717  dvfgg  15914  incistruhgr  16536  edgssv2en  16645  wksfval  16768