Theorem sseq2d 2079

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 2073	. 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 953   (_ wss 2037

This theorem is referenced by:  sseq12d 2080  sseqtrd 2087  funimass2 3559  fnco 3581  fnssresb 3585  fco 3621  f1ores 3688  tz6.12-2 3724  ssimaexg 3754  isofrlem 3886  oaordi 4164  oawordeulem 4172  oaass 4179  odi 4194  omass 4195  oen0 4197  oelim2 4206  pmvalg 4315  pw2en 4426  sbthlem2 4428  sbth 4437  ssenen 4484  phplem2 4489  pssnn 4513  ssfi 4515  fiint 4534  fodomfi 4540  trcl 4617  r1tr 4626  rankeq0 4668  rankr1id 4669  rankr1b 4671  kmlem5 4741  alephordlem2 4845  alephordi 4846  alephgeom 4854  cardaleph 4857  cardalephex 4858  cflim 4881  isbasisg 7553  tgvalt 7558  cldval 7608  ntrfval 7609  clsfval 7610  neifval 7655  neiint 7660  lpfval 7683  cncnplem4 7716  opnfval 7797  neibl 7817  lpbl 7819  metcnp 7826  lmfval 7863  caufval 7864  metelcls 7900  metcld 7901  cmsss 7931  bcthlem15 7947  bcth 7966  sspval 8316  hsupunss 9228  spanss2 9229  orthin 9285  chssoct 9334  chsscon3t 9338  chsscon1t 9339  h1datomt 9422  pjoml6 9449  osumlem8 9502  osumt 9505  spansncvt 9515  pjcjt2 9554  pjopytht 9582  hstel2t 10056  hstlet 10067  stjt 10072  mdslmd1lem1 10160  atordt 10223  irredlem4 10228  atcvat4 10232  mdsymlem2 10239  mdsymlem3 10240  mdsymlem8 10245  mdsym 10246  ghomfo 10296  abfi2 10378  oefil2 10441  fgsb 10444  fgsb2 10449  ishgrag 10605  hgralem 10606  ispgrag 10615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain