Theorem sseq2d 3633

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseq12d  3634  sseqtrd  3641  sbcrel  5205  funimass2  5972  fnco  5999  fnssresb  6003  fnimaeq0  6013  foimacnv  6154  fvelimab  6253  ssimaexg  6264  knatar  6607  wfrdmcl  7423  wfrlem12  7426  onfununi  7438  oaordi  7626  oawordeulem  7634  oaass  7641  odi  7659  omass  7660  oen0  7666  oelim2  7675  nnaordi  7698  nnawordex  7717  pssnn  8178  fissuni  8271  dffi3  8337  cantnfle  8568  cantnflem1  8586  trcl  8604  r1sdom  8637  iscard2  8802  alephordi  8897  alephgeom  8905  cardaleph  8912  cardalephex  8913  ackbij2lem4  9064  cflm  9072  cfslbn  9089  cofsmo  9091  cfsmolem  9092  cfcoflem  9094  coftr  9095  alephsing  9098  fin23lem28  9162  fin23lem30  9164  fin23lem33  9167  fin1a2lem9  9230  axdc3lem2  9273  ttukeylem5  9335  fpwwe2lem5  9456  pwfseqlem4a  9483  pwfseqlem4  9484  wunex2  9560  inar1  9597  sstskm  9664  fsuppmapnn0fiubex  12792  swrdnd  13432  swrd0  13434  repswswrd  13531  rtrclreclem1  13798  rtrclreclem2  13799  summolem2  14447  summo  14448  zsum  14449  sumz  14453  sumss  14455  fsumcvg3  14460  prodmolem2  14665  prodmo  14666  zprod  14667  prod1  14674  vdwlem1  15685  vdwlem12  15696  vdwlem13  15697  ramub2  15718  rami  15719  ramz2  15728  setsstruct2  15896  prdsval  16115  pwsle  16152  mrcuni  16281  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  eqgfval  17642  sscntz  17759  resscntz  17764  lsmlub  18078  efgrelexlemb  18163  efgcpbllemb  18168  gsumval3a  18304  gsumzaddlem  18321  gsumzoppg  18344  dmdprd  18397  dprdcntz  18407  subgdmdprd  18433  subrgpropd  18814  islss  18935  lsslss  18961  lsspropd  19017  lsmelpr  19091  lbspropd  19099  ltbval  19471  opsrval  19474  lsslinds  20170  isbasisg  20751  tgval  20759  tgss3  20790  restbas  20962  tgrest  20963  restcld  20976  restopn2  20981  restntr  20986  cnpnei  21068  cncls2  21077  perfcls  21169  cmpsublem  21202  cmpsub  21203  cmpcld  21205  uncmp  21206  hauscmplem  21209  cmpfi  21211  nconnsubb  21226  clsconn  21233  hausllycmp  21297  1stckgenlem  21356  txbas  21370  ptbasfi  21384  txcnpi  21411  ptcnp  21425  txcmplem1  21444  txcmplem2  21445  xkococnlem  21462  qtopcld  21516  fbasssin  21640  fbssint  21642  fbun  21644  fbasrn  21688  filufint  21724  ufinffr  21733  ufildr  21735  ustval  22006  trust  22033  elmopn  22247  neibl  22306  cfilucfil  22364  icccmplem1  22625  icccmplem2  22626  bndth  22757  isphtpc  22793  metcld  23104  bcthlem1  23121  bcth  23126  ovolfioo  23236  ovolficc  23237  elovolmr  23244  ovoliunlem3  23272  ovolicc2  23290  volsuplem  23323  dyadmax  23366  dyadmbllem  23367  dyadmbl  23368  incistruhgr  25974  edgssv2  26090  wksfval  26505  2wlkdlem9  26830  3wlkdlem9  27028  isfrgr  27122  sspval  27578  ubth  27729  orthin  28305  chssoc  28355  chsscon3  28359  chsscon1  28360  h1datom  28441  pjoml6i  28448  osum  28504  spansncv  28512  pjcjt2  28551  pjopyth  28579  hstel2  29078  hstle  29089  stj  29094  dmdbr5  29167  mdslmd1lem1  29184  atord  29247  chirredlem4  29252  atcvat4i  29256  mdsymlem2  29263  mdsymlem3  29264  mdsymlem8  29269  padct  29497  ssnnssfz  29549  tpr2rico  29958  ordtrestNEW  29967  sigaval  30173  issiga  30174  issgon  30186  oms0  30359  omssubadd  30362  kur14  31198  cvmliftlem15  31280  mclsrcl  31458  mclsval  31460  trpredtr  31730  dftrpred3g  31733  frrlem5e  31788  ivthALT  32330  isfne  32334  topfne  32349  neibastop3  32357  tailfb  32372  filnetlem1  32373  filnetlem4  32376  csbwrecsg  33173  relowlssretop  33211  poimirlem24  33433  mblfinlem2  33447  sstotbnd2  33573  sstotbnd  33574  sstotbnd3  33575  ssbnd  33587  cntotbnd  33595  cnpwstotbnd  33596  ismtyres  33607  heibor1lem  33608  heiborlem1  33610  heiborlem6  33615  heiborlem8  33617  exidreslem  33676  scottexf  33976  scott0f  33977  lshpcmp  34275  lsmsat  34295  lsmsatcv  34297  lfl1dim  34408  lfl1dim2N  34409  lkrss2N  34456  psubspset  35030  paddss  35131  psubclsetN  35222  dilfsetN  35439  dilsetN  35440  diaglbN  36344  dibglbN  36455  dihlspsnat  36622  dihglb2  36631  dochffval  36638  dochfval  36639  dochvalr  36646  dochord2N  36660  dochsncom  36671  dihjat1lem  36717  dvh4dimat  36727  dvh3dimatN  36728  dvh2dimatN  36729  dochexmidlem1  36749  lpolsetN  36771  lpolconN  36776  hdmaplkr  37205  hdmapoc  37223  hlhillcs  37250  ismrc  37264  incssnn0  37274  nacsfix  37275  hbt  37700  ss2iundf  37951  clsk1indlem1  38343  clsk1independent  38344  isotone1  38346  isotone2  38347  ntrclsiso  38365  ntrclsk2  38366  ssinc  39264  uzfissfz  39542  stoweidlem50  40267  stoweidlem57  40274  fourierdlem20  40344  fourierdlem50  40373  fourierdlem64  40387  fourierdlem86  40409  fourierdlem103  40426  fourierdlem104  40427  ovnval  40755  hoicvrrex  40770  ovnlecvr  40772  ovncvrrp  40778  ovnsubaddlem1  40784  hoidmvlelem3  40811  hoidmvle  40814  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  ovncvr2  40825  hspmbl  40843  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovollem1  40870  ovnovollem2  40871  sprsymrelfvlem  41740  uspgrsprf  41754  uspgrsprfo  41756  ssnn0ssfz  42127  lincfsuppcl  42202