Theorem sseq2d 3254

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 3248	. 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 1395   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseq12d  3255  sseqtrd  3262  exmidsssn  4285  exmidsssnc  4286  onsucsssucexmid  4618  sbcrel  4804  funimass2  5398  fnco  5430  fnssresb  5434  fnimaeq0  5444  foimacnv  5589  fvelimab  5689  ssimaexg  5695  fvmptss2  5708  rdgss  6527  tapeq2  7435  fzowrddc  11174  swrdnd  11186  swrd0g  11187  summodclem2  11888  summodc  11889  zsumdc  11890  fsum3cvg3  11902  prodmodclem2  12083  prodmodc  12084  zproddc  12085  ennnfoneleminc  12977  tgval  13290  prdsval  13301  releqgg  13752  eqgex  13753  eqgfval  13754  opprsubgg  14042  unitsubm  14077  subrngpropd  14174  subrgsubm  14192  issubrg3  14205  subrgpropd  14211  lsslss  14339  lsspropdg  14389  islidlm  14437  rspcl  14449  rspssid  14450  isbasisg  14712  tgss3  14746  restbasg  14836  tgrest  14837  restopn2  14851  cnpnei  14887  cnptopresti  14906  txbas  14926  elmopn  15114  neibl  15159  dvfgg  15356  incistruhgr  15884  edgssv2en  15991  wksfval  16028