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  6659  isfsuppfi  7296  funisfsuppdc  7298  papeq2  7616  tapeq2  7625  fzowrddc  11440  swrdnd  11452  swrd0g  11453  summodclem2  12173  summodc  12174  zsumdc  12175  fsum3cvg3  12187  prodmodclem2  12368  prodmodc  12369  zproddc  12370  ennnfoneleminc  13359  tgval  13674  releqgg  14081  eqgex  14082  eqgfval  14083  sscntz  14157  resscntz  14165  prdsval  14279  opprsubgg  14498  unitsubm  14534  subrngpropd  14632  subrgsubm  14650  issubrg3  14663  subrgpropd  14669  lsslss  14826  lsspropdg  14876  islidlm  14924  rspcl  14936  rspssid  14937  mplsubgfilemcl  15232  mplsubgfileminv  15233  isbasisg  15287  tgss3  15321  restbasg  15411  tgrest  15412  restopn2  15426  cnpnei  15462  cnptopresti  15481  txbas  15501  elmopn  15689  neibl  15734  dvfgg  15931  incistruhgr  16553  edgssv2en  16662  wksfval  16785