Theorem sseq2d 2645

Description: An equality deduction for the subclass relationship.

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 2639	. 2 |- (A = B -> (C C_ A <-> C C_ B))
3	1, 2	syl 12	1 |- (ph -> (C C_ A <-> C C_ B))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   C_ wss 2593

This theorem is referenced by:  sseq12d 2646  sseqtrd 2653  unissint 3241  funimass2 4492  fnco 4521  fnssresb 4525  fcoOLD 4574  f1ores 4654  foimacnv 4657  resdif 4659  tz6.12-2 4696  fvelimab 4725  ssimaexg 4730  isofrlem 4878  onfununi 5116  oaordi 5227  oawordeulem 5236  oaass 5243  odi 5258  omass 5259  oen0 5261  oelim2 5270  pmvalg 5390  pw2en 5505  sbthlem2 5511  sbth 5520  ssenen 5598  phplem2 5603  pssnn 5628  ssfi 5630  fiint 5650  fodomfi 5656  trcl 5752  r1tr 5765  rankeq0 5807  rankr1id 5808  rankr1b 5810  kmlem5 5931  alephordlem2 6021  alephordi 6022  alephgeom 6030  cardaleph 6033  cardalephex 6034  cflim 6057  isbasisg 8880  tgval 8886  cldval 8942  ntrfval 8943  clsfval 8944  neifval 8990  neiint 8995  lpfval 9018  cnpnei 9043  cncnplem4 9054  opnfval 9134  neibl 9154  lpbl 9157  metequiv 9158  metcnp 9165  lmfval 9203  caufval 9204  metelcls 9243  metcld 9245  cmsss 9275  bcthlem15 9291  bcth 9310  sspval 9721  fipreima 10175  abfi2 10216  stoig 10251  subcld 10254  isfil 10266  oefil2 10275  fbasssin 10278  fbssint 10279  fbfgss 10288  fgfil 10290  filrn 10293  elfilmap 10312  hsupunss 10946  spanss2 10947  orthin 11003  chssoc 11052  chsscon3 11056  chsscon1 11057  h1datom 11138  pjoml6i 11165  osumlem8 11220  osum 11223  spansncv 11233  pjcjt2 11272  pjopyth 11300  hstel2 11791  hstle 11802  stj 11807  dmdbr5 11880  mdslmd1lem1 11897  atord 11960  irredlem4 11965  atcvat4i 11969  mdsymlem2 11976  mdsymlem3 11977  mdsymlem8 11982  mdsymi 11983  ghomfo 13634  trcltr 13936  wfrlem9 13965  wfrlem12 13968  onsubcum 14442  inpc 14619  ptincpw 14912  fgsb 14921  fgsb2 14925  topsinind 14967  tpgprop1 14986  tpgprop2 14987  lvsovso 15038  issubcat 15193  bpmp 15251  fictblem 15370  subntr 15425  compsublem 15430  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  connsub 15443  reconnlem1 15446  ivthALT 15454  isfne 15480  locfincf 15516  neibastop1 15518  neibastop2lem4 15522  topmeet 15526  neifg 15559  ufileu 15573  filufint 15574  ufinffr 15578  cnpfillim 15589  fmfnfmlem4 15597  flimfnfcls 15615  fcluscomplem 15620  tailfb 15639  raleqfn 15672  fipreimaOLD 15756  sstotbnd 15936  ismtyhmeolem 15950  ismtyres 15954  heiborlem20 15974  heiborlem21 15975  heiborlem23 15977  heiborlem38 15992  heiborlem42 15996  rrntotbnd 16022  rrnheibor 16023  exidreslem 16030  divrngcl 16110  isdivrng2 16111  keridl 16180  igenss 16210  ishgrag 16291  hgralem 16292  ispgrag 16301  isclat 16888  csubspset 17208  psubspset 17225  paddss 17306  psubclset 17346  dilfset 17401  dilset 17402

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain