Theorem sseq2d 3268

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 3262	. 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 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  sseq12d  3269  sseqtrd  3276  exmidsssn  4315  exmidsssnc  4316  onsucsssucexmid  4649  sbcrel  4836  funimass2  5434  fnco  5466  fnssresb  5470  fnimaeq0  5480  foimacnv  5632  fvelimab  5733  ssimaexg  5739  fvmptss2  5752  rdgss  6614  tapeq2  7567  fzowrddc  11339  swrdnd  11351  swrd0g  11352  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3cvg3  12082  prodmodclem2  12263  prodmodc  12264  zproddc  12265  ennnfoneleminc  13162  tgval  13475  prdsval  13486  releqgg  13937  eqgex  13938  eqgfval  13939  opprsubgg  14228  unitsubm  14264  subrngpropd  14361  subrgsubm  14379  issubrg3  14392  subrgpropd  14398  lsslss  14529  lsspropdg  14579  islidlm  14627  rspcl  14639  rspssid  14640  isbasisg  14909  tgss3  14943  restbasg  15033  tgrest  15034  restopn2  15048  cnpnei  15084  cnptopresti  15103  txbas  15123  elmopn  15311  neibl  15356  dvfgg  15553  incistruhgr  16085  edgssv2en  16194  wksfval  16317