Theorem sseq2d 3258

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 3252	. 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 1398   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12d  3259  sseqtrd  3266  exmidsssn  4298  exmidsssnc  4299  onsucsssucexmid  4631  sbcrel  4818  funimass2  5415  fnco  5447  fnssresb  5451  fnimaeq0  5461  foimacnv  5610  fvelimab  5711  ssimaexg  5717  fvmptss2  5730  rdgss  6592  tapeq2  7515  fzowrddc  11277  swrdnd  11289  swrd0g  11290  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3cvg3  12020  prodmodclem2  12201  prodmodc  12202  zproddc  12203  ennnfoneleminc  13095  tgval  13408  prdsval  13419  releqgg  13870  eqgex  13871  eqgfval  13872  opprsubgg  14161  unitsubm  14197  subrngpropd  14294  subrgsubm  14312  issubrg3  14325  subrgpropd  14331  lsslss  14460  lsspropdg  14510  islidlm  14558  rspcl  14570  rspssid  14571  isbasisg  14838  tgss3  14872  restbasg  14962  tgrest  14963  restopn2  14977  cnpnei  15013  cnptopresti  15032  txbas  15052  elmopn  15240  neibl  15285  dvfgg  15482  incistruhgr  16014  edgssv2en  16123  wksfval  16246