Theorem sseq2d 2085

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 2079	. 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 954   (_ wss 2043

This theorem is referenced by:  sseq12d 2086  sseqtrd 2093  funimass2 3565  fnco 3587  fnssresb 3591  fco 3627  f1ores 3694  tz6.12-2 3730  ssimaexg 3760  isofrlem 3892  oaordi 4170  oawordeulem 4178  oaass 4185  odi 4200  omass 4201  oen0 4203  oelim2 4212  pmvalg 4321  pw2en 4432  sbthlem2 4434  sbth 4443  ssenen 4490  phplem2 4495  pssnn 4519  ssfi 4521  fiint 4540  fodomfi 4546  trcl 4625  r1tr 4634  rankeq0 4676  rankr1id 4677  rankr1b 4679  kmlem5 4749  alephordlem2 4853  alephordi 4854  alephgeom 4862  cardaleph 4865  cardalephex 4866  cflim 4889  isbasisg 7561  tgvalt 7566  cldval 7616  ntrfval 7617  clsfval 7618  neifval 7664  neiint 7669  lpfval 7692  cncnplem4 7727  opnfval 7809  neibl 7829  lpbl 7832  metcnp 7839  lmfval 7877  caufval 7878  metelcls 7916  metcld 7917  cmsss 7947  bcthlem15 7963  bcth 7982  sspval 8329  hsupunss 9251  spanss2 9252  orthin 9308  chssoct 9357  chsscon3t 9361  chsscon1t 9362  h1datomt 9445  pjoml6 9472  osumlem8 9525  osumt 9528  spansncvt 9538  pjcjt2 9577  pjopytht 9605  hstel2t 10084  hstlet 10095  stjt 10100  mdslmd1lem1 10189  atordt 10252  irredlem4 10257  atcvat4 10261  mdsymlem2 10268  mdsymlem3 10269  mdsymlem8 10274  mdsym 10275  ghomfo 10325  abfi2 10414  oefil2 10477  fgsb 10480  fgsb2 10485  ishgrag 10641  hgralem 10642  ispgrag 10651

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain