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

Theorem sseq2d 3336
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 3330 . 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 1649    C_ wss 3280
This theorem is referenced by:  sseq12d  3337  sseqtrd  3344  funimass2  5486  fnco  5512  fnssresb  5516  fnimaeq0  5525  foimacnv  5651  fvelimab  5741  ssimaexg  5748  knatar  6039  onfununi  6562  oaordi  6748  oawordeulem  6756  oaass  6763  odi  6781  omass  6782  oen0  6788  oelim2  6797  nnaordi  6820  nnawordex  6839  pssnn  7286  fissuni  7369  dffi3  7394  cantnfle  7582  cantnflem1  7601  trcl  7620  r1sdom  7656  iscard2  7819  alephordi  7911  alephgeom  7919  cardaleph  7926  cardalephex  7927  ackbij2lem4  8078  cflm  8086  cfslbn  8103  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  coftr  8109  alephsing  8112  fin23lem28  8176  fin23lem30  8178  fin23lem33  8181  fin1a2lem9  8244  axdc3lem2  8287  ttukeylem5  8349  fpwwe2lem5  8465  pwfseqlem4a  8492  pwfseqlem4  8493  wunex2  8569  inar1  8606  sstskm  8673  summolem2  12465  summo  12466  zsum  12467  sumz  12471  sumss  12473  fsumcvg3  12478  vdwlem1  13304  vdwlem12  13315  vdwlem13  13316  ramub2  13337  rami  13338  ramz2  13347  prdsval  13633  pwsle  13669  mrcuni  13801  isclat  14493  gsumpropd  14731  gsumress  14732  eqgfval  14943  sscntz  15080  resscntz  15085  lsmlub  15252  efgrelexlemb  15337  efgcpbllemb  15342  gsumval3a  15467  dmdprd  15514  dprdcntz  15521  subgdmdprd  15547  subrgpropd  15857  islss  15966  lsslss  15992  lsspropd  16048  lsmelpr  16118  lbspropd  16126  ltbval  16487  opsrval  16490  isbasisg  16967  tgval  16975  tgss3  17006  restbas  17176  tgrest  17177  restcld  17190  restopn2  17195  restntr  17200  cnpnei  17282  cncls2  17291  perfcls  17383  cmpsublem  17416  cmpsub  17417  cmpcld  17419  uncmp  17420  hauscmplem  17423  cmpfi  17425  nconsubb  17439  clscon  17446  hausllycmp  17510  1stckgenlem  17538  txbas  17552  ptbasfi  17566  txcnpi  17593  ptcnp  17607  txcmplem1  17626  txcmplem2  17627  xkococnlem  17644  qtopcld  17698  fbasssin  17821  fbssint  17823  fbun  17825  fbasrn  17869  filufint  17905  ufinffr  17914  ufildr  17916  ustval  18185  trust  18212  elmopn  18425  neibl  18484  cfilucfilOLD  18552  cfilucfil  18553  icccmplem1  18806  icccmplem2  18807  bndth  18936  isphtpc  18972  metcld  19211  bcthlem1  19230  bcth  19235  ovolfioo  19317  ovolficc  19318  elovolmr  19325  ovoliunlem3  19353  ovolicc2  19371  volsuplem  19402  dyadmax  19443  dyadmbllem  19444  dyadmbl  19445  sspval  22175  ubth  22328  orthin  22901  chssoc  22951  chsscon3  22955  chsscon1  22956  h1datom  23037  pjoml6i  23044  osum  23100  spansncv  23108  pjcjt2  23147  pjopyth  23175  hstel2  23675  hstle  23686  stj  23691  dmdbr5  23764  mdslmd1lem1  23781  atord  23844  chirredlem4  23849  atcvat4i  23853  mdsymlem2  23860  mdsymlem3  23861  mdsymlem8  23866  ssnnssfz  24101  gsumpropd2lem  24173  tpr2rico  24263  sigaval  24446  issiga  24447  issgon  24459  kur14  24855  cvmliftlem15  24938  ghomfo  25055  rtrclreclem.refl  25097  rtrclreclem.subset  25098  prodmolem2  25214  prodmo  25215  zprod  25216  prod1  25223  trpredtr  25447  dftrpred3g  25450  wfrlem9  25478  wfrlem12  25481  frrlem5e  25503  nofulllem1  25570  nofulllem2  25571  mblfinlem  26143  ivthALT  26228  isfne  26238  topfne  26260  neibastop3  26281  tailfb  26296  filnetlem1  26297  filnetlem4  26300  sstotbnd2  26373  sstotbnd  26374  sstotbnd3  26375  ssbnd  26387  cntotbnd  26395  cnpwstotbnd  26396  ismtyres  26407  heibor1lem  26408  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  exidreslem  26442  ismrc  26645  incssnn0  26655  nacsfix  26656  lsslinds  27169  hbt  27202  stoweidlem50  27666  stoweidlem57  27673  sbcrel  27848  swrdnd  28001  isfrgra  28094  lshpcmp  29471  lsmsat  29491  lsmsatcv  29493  lfl1dim  29604  lfl1dim2N  29605  lkrss2N  29652  psubspset  30226  paddss  30327  psubclsetN  30418  dilfsetN  30634  dilsetN  30635  diaglbN  31538  dibglbN  31649  dihlspsnat  31816  dihglb2  31825  dochffval  31832  dochfval  31833  dochvalr  31840  dochord2N  31854  dochsncom  31865  dihjat1lem  31911  dvh4dimat  31921  dvh3dimatN  31922  dvh2dimatN  31923  dochexmidlem1  31943  lpolsetN  31965  lpolconN  31970  hdmaplkr  32399  hdmapoc  32417  hlhillcs  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator