Theorem sseq2d 2089

Description: An equality deduction for the subclass relationship.

Hypothesis

Ref	Expression
sseq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
sseq2d	|- (ph -> (C (_ A <-> C (_ B))

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- (ph -> A = B)
2		sseq2 2083	. 2 |- (A = B -> (C (_ A <-> C (_ B))
3	1, 2	syl 10	1 |- (ph -> (C (_ A <-> C (_ B))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   (_ wss 2047

This theorem is referenced by:  sseq12d 2090  sseqtrd 2097  funimass2 3573  fnco 3595  fnssresb 3599  fco 3636  f1ores 3703  tz6.12-2 3739  ssimaexg 3769  isofrlem 3901  oaordi 4180  oawordeulem 4188  oaass 4195  odi 4210  omass 4211  oen0 4213  oelim2 4222  pmvalg 4331  pw2en 4444  sbthlem2 4446  sbth 4455  ssenen 4502  phplem2 4507  pssnn 4531  ssfi 4533  fiint 4552  fodomfi 4558  trcl 4637  r1tr 4646  rankeq0 4688  rankr1id 4689  rankr1b 4691  kmlem5 4761  alephordlem2 4865  alephordi 4866  alephgeom 4874  cardaleph 4877  cardalephex 4878  cflim 4901  isbasisg 7596  tgvalt 7601  cldval 7651  ntrfval 7652  clsfval 7653  neifval 7699  neiint 7704  lpfval 7727  cncnplem4 7762  opnfval 7842  neibl 7862  lpbl 7865  metcnp 7872  lmfval 7910  caufval 7911  metelcls 7950  metcld 7952  cmsss 7982  bcthlem15 7998  bcth 8017  sspval 8367  hsupunss 9298  spanss2 9299  orthin 9355  chssoct 9404  chsscon3t 9408  chsscon1t 9409  h1datomt 9490  pjoml6 9517  osumlem8 9570  osumt 9573  spansncvt 9583  pjcjt2 9622  pjopytht 9650  hstel2t 10131  hstlet 10142  stjt 10147  dmdbr5 10220  mdslmd1lem1 10237  atordt 10300  irredlem4 10305  atcvat4 10309  mdsymlem2 10316  mdsymlem3 10317  mdsymlem8 10322  mdsym 10323  ghomfo 10376  abfi2 10463  oefil2 10526  fgsb 10529  fgsb2 10535  ishgrag 10705  hgralem 10706  ispgrag 10715

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain