Theorem sseq1d 2644

Description: An equality deduction for the subclass relationship.

Hypothesis

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

Assertion

Ref	Expression
sseq1d	|- (ph -> (A C_ C <-> B C_ C))

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- (ph -> A = B)
2		sseq1 2637	. 2 |- (A = B -> (A C_ C <-> B C_ C))
3	1, 2	syl 12	1 |- (ph -> (A C_ C <-> B C_ C))

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

This theorem is referenced by:  sseq12d 2646  eqsstrd 2651  snssg 3124  prssgOLD 3141  ssiun2s 3297  treq 3417  ordunel 3906  dmxpss 4343  rnxpssOLD 4345  funimass1 4491  feq1 4551  fvimacnvi 4777  fvimacnvALT 4782  oaordi 5227  oaword2 5235  oawordeulem 5236  omwordri 5251  omword1 5252  oewordri 5267  oeordsuc 5269  ereq 5324  map0e 5401  ac6sfi 5509  sbthlem5 5514  fodomr 5547  ordtypelem6 5689  ordtypelem7 5690  inf3lema 5715  inf3lemd 5718  trcl 5752  r1val1 5769  rankr1 5785  rankxplim 5823  scottex 5846  scott0 5847  scottexs 5848  scott0s 5849  karden 5856  cardaleph 6033  cfub 6056  cflecard 6060  cfle 6061  peano5uzti 7416  infmap2lem2 8849  iscnp 9036  cnsscnp 9049  blss 9130  ssblex 9133  opnin 9146  blnei 9156  metcnp 9165  tgioolem 9192  bcthlem9 9285  bcthlem15 9291  bcthlem18 9294  bcthlem28 9304  bcth 9310  subgrnss 9428  sspval 9721  isssp 9722  grothpw 10134  grothpwex 10135  axgroth6 10137  subtopmet 10256  sfvlim 10296  isfillim 10298  elfilmap 10312  elfilmap2 10313  elfilmap3 10314  ocsh 10789  hsupval2 10933  chsupid 10944  chsupsn 10945  shlub 10987  shmodi 10996  chsscon3 11056  chsscon2 11058  spansncvi 11232  pj3i 11781  mdslmd1lem3 11899  mdslmd1lem4 11900  mdsymlem5 11979  sumdmdlem2 11991  dmdbr5ati 11994  dmdbr6ati 11995  dmdbr7ati 11996  bnj220 12511  bnj897 12817  bnj1014 13374  bnj1015 13375  bnj1069 13400  bnj1081 13407  bnj1123 13422  bnj1134 13427  bnj1125 13430  bnj1137 13433  bnj1287 13477  bnj1288 13478  bnj1450 13541  bnj1462 13546  suprzcl 13658  preddowncl 13907  trcllem1 13933  frxp 13951  wfrlem1 13957  wfrlem3 13959  wfrlem9 13965  wfrlem15 13971  tfrALTlem 13976  axfelem7 14037  axfelem8 14038  axfelem9 14039  axfelem15 14045  fopab2g 14485  preoref22 14570  osneisi 14875  ptincpw 14912  limfillem2 14939  plimfil 14940  conttnf 14944  iscnp3 14946  topsinind 14967  altretop 14997  iintlem2 15011  supbrr 15048  isalg 15068  algi 15074  issubcat 15193  issubcata 15194  issubcatb 15195  taralt 15211  tarax1 15216  tartarmap 15265  finsschain 15373  ordtypelem6OLD 15380  ordtypelem7OLD 15381  connsub 15443  reconnlem1 15446  reconn 15451  ivthALT 15454  neibastop2lem1 15519  topmeet 15526  imaelfm 15591  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem4 15597  flimfbas 15601  isfclus 15606  filnet 15645  fimax 15746  inficl 15757  txmet 15925  totbndss 15937  heiborlem6 15960  heiborlem13 15967  heiborlem23 15977  recms 16010  smoge 16454  paddasslem17 17297

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