MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq2d Structured version   Unicode version

Theorem sseq2d 3368
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
StepHypRef Expression
1 sseq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sseq2 3362 . 2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C  C_  A  <->  C 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    C_ wss 3312
This theorem is referenced by:  sseq12d  3369  sseqtrd  3376  funimass2  5519  fnco  5545  fnssresb  5549  fnimaeq0  5558  foimacnv  5684  fvelimab  5774  ssimaexg  5781  knatar  6072  onfununi  6595  oaordi  6781  oawordeulem  6789  oaass  6796  odi  6814  omass  6815  oen0  6821  oelim2  6830  nnaordi  6853  nnawordex  6872  pssnn  7319  fissuni  7403  dffi3  7428  cantnfle  7618  cantnflem1  7637  trcl  7656  r1sdom  7692  iscard2  7855  alephordi  7947  alephgeom  7955  cardaleph  7962  cardalephex  7963  ackbij2lem4  8114  cflm  8122  cfslbn  8139  cofsmo  8141  cfsmolem  8142  cfcoflem  8144  coftr  8145  alephsing  8148  fin23lem28  8212  fin23lem30  8214  fin23lem33  8217  fin1a2lem9  8280  axdc3lem2  8323  ttukeylem5  8385  fpwwe2lem5  8501  pwfseqlem4a  8528  pwfseqlem4  8529  wunex2  8605  inar1  8642  sstskm  8709  summolem2  12502  summo  12503  zsum  12504  sumz  12508  sumss  12510  fsumcvg3  12515  vdwlem1  13341  vdwlem12  13352  vdwlem13  13353  ramub2  13374  rami  13375  ramz2  13384  prdsval  13670  pwsle  13706  mrcuni  13838  isclat  14530  gsumpropd  14768  gsumress  14769  eqgfval  14980  sscntz  15117  resscntz  15122  lsmlub  15289  efgrelexlemb  15374  efgcpbllemb  15379  gsumval3a  15504  dmdprd  15551  dprdcntz  15558  subgdmdprd  15584  subrgpropd  15894  islss  16003  lsslss  16029  lsspropd  16085  lsmelpr  16155  lbspropd  16163  ltbval  16524  opsrval  16527  isbasisg  17004  tgval  17012  tgss3  17043  restbas  17214  tgrest  17215  restcld  17228  restopn2  17233  restntr  17238  cnpnei  17320  cncls2  17329  perfcls  17421  cmpsublem  17454  cmpsub  17455  cmpcld  17457  uncmp  17458  hauscmplem  17461  cmpfi  17463  nconsubb  17478  clscon  17485  hausllycmp  17549  1stckgenlem  17577  txbas  17591  ptbasfi  17605  txcnpi  17632  ptcnp  17646  txcmplem1  17665  txcmplem2  17666  xkococnlem  17683  qtopcld  17737  fbasssin  17860  fbssint  17862  fbun  17864  fbasrn  17908  filufint  17944  ufinffr  17953  ufildr  17955  ustval  18224  trust  18251  elmopn  18464  neibl  18523  cfilucfilOLD  18591  cfilucfil  18592  icccmplem1  18845  icccmplem2  18846  bndth  18975  isphtpc  19011  metcld  19250  bcthlem1  19269  bcth  19274  ovolfioo  19356  ovolficc  19357  elovolmr  19364  ovoliunlem3  19392  ovolicc2  19410  volsuplem  19441  dyadmax  19482  dyadmbllem  19483  dyadmbl  19484  sspval  22214  ubth  22367  orthin  22940  chssoc  22990  chsscon3  22994  chsscon1  22995  h1datom  23076  pjoml6i  23083  osum  23139  spansncv  23147  pjcjt2  23186  pjopyth  23214  hstel2  23714  hstle  23725  stj  23730  dmdbr5  23803  mdslmd1lem1  23820  atord  23883  chirredlem4  23888  atcvat4i  23892  mdsymlem2  23899  mdsymlem3  23900  mdsymlem8  23905  ssnnssfz  24140  gsumpropd2lem  24212  tpr2rico  24302  sigaval  24485  issiga  24486  issgon  24498  kur14  24894  cvmliftlem15  24977  ghomfo  25094  rtrclreclem.refl  25136  rtrclreclem.subset  25137  prodmolem2  25253  prodmo  25254  zprod  25255  prod1  25262  trpredtr  25500  dftrpred3g  25503  wfrlem9  25538  wfrlem12  25541  frrlem5e  25582  nofulllem1  25649  nofulllem2  25650  mblfinlem  26234  ivthALT  26329  isfne  26339  topfne  26361  neibastop3  26382  tailfb  26397  filnetlem1  26398  filnetlem4  26401  sstotbnd2  26474  sstotbnd  26475  sstotbnd3  26476  ssbnd  26488  cntotbnd  26496  cnpwstotbnd  26497  ismtyres  26508  heibor1lem  26509  heiborlem1  26511  heiborlem6  26516  heiborlem8  26518  exidreslem  26543  ismrc  26746  incssnn0  26756  nacsfix  26757  lsslinds  27269  hbt  27302  stoweidlem50  27766  stoweidlem57  27773  sbcrel  27948  swrdnd  28154  isfrgra  28317  lshpcmp  29723  lsmsat  29743  lsmsatcv  29745  lfl1dim  29856  lfl1dim2N  29857  lkrss2N  29904  psubspset  30478  paddss  30579  psubclsetN  30670  dilfsetN  30886  dilsetN  30887  diaglbN  31790  dibglbN  31901  dihlspsnat  32068  dihglb2  32077  dochffval  32084  dochfval  32085  dochvalr  32092  dochord2N  32106  dochsncom  32117  dihjat1lem  32163  dvh4dimat  32173  dvh3dimatN  32174  dvh2dimatN  32175  dochexmidlem1  32195  lpolsetN  32217  lpolconN  32222  hdmaplkr  32651  hdmapoc  32669  hlhillcs  32696
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator