Theorem sseq2d 3223

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 3217	. 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 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sseq12d  3224  sseqtrd  3231  exmidsssn  4246  exmidsssnc  4247  onsucsssucexmid  4575  sbcrel  4761  funimass2  5352  fnco  5384  fnssresb  5388  fnimaeq0  5397  foimacnv  5540  fvelimab  5635  ssimaexg  5641  fvmptss2  5654  rdgss  6469  tapeq2  7365  fzowrddc  11100  swrdnd  11112  swrd0g  11113  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3cvg3  11707  prodmodclem2  11888  prodmodc  11889  zproddc  11890  ennnfoneleminc  12782  tgval  13094  prdsval  13105  releqgg  13556  eqgex  13557  eqgfval  13558  opprsubgg  13846  unitsubm  13881  subrngpropd  13978  subrgsubm  13996  issubrg3  14009  subrgpropd  14015  lsslss  14143  lsspropdg  14193  islidlm  14241  rspcl  14253  rspssid  14254  isbasisg  14516  tgss3  14550  restbasg  14640  tgrest  14641  restopn2  14655  cnpnei  14691  cnptopresti  14710  txbas  14730  elmopn  14918  neibl  14963  dvfgg  15160