Theorem sseq2d 3222

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 3216	. 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 1372   C_ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sseq12d  3223  sseqtrd  3230  exmidsssn  4245  exmidsssnc  4246  onsucsssucexmid  4574  sbcrel  4760  funimass2  5351  fnco  5383  fnssresb  5387  fnimaeq0  5396  foimacnv  5539  fvelimab  5634  ssimaexg  5640  fvmptss2  5653  rdgss  6468  tapeq2  7364  summodclem2  11664  summodc  11665  zsumdc  11666  fsum3cvg3  11678  prodmodclem2  11859  prodmodc  11860  zproddc  11861  ennnfoneleminc  12753  tgval  13065  prdsval  13076  releqgg  13527  eqgex  13528  eqgfval  13529  opprsubgg  13817  unitsubm  13852  subrngpropd  13949  subrgsubm  13967  issubrg3  13980  subrgpropd  13986  lsslss  14114  lsspropdg  14164  islidlm  14212  rspcl  14224  rspssid  14225  isbasisg  14487  tgss3  14521  restbasg  14611  tgrest  14612  restopn2  14626  cnpnei  14662  cnptopresti  14681  txbas  14701  elmopn  14889  neibl  14934  dvfgg  15131