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

Theorem sseq2d 3292
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 3286 . 2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
31, 2syl 15 1  |-  ( ph  ->  ( C  C_  A  <->  C 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1647    C_ wss 3238
This theorem is referenced by:  sseq12d  3293  sseqtrd  3300  funimass2  5431  fnco  5457  fnssresb  5461  fnimaeq0  5470  foimacnv  5596  fvelimab  5685  ssimaexg  5692  knatar  5980  onfununi  6500  oaordi  6686  oawordeulem  6694  oaass  6701  odi  6719  omass  6720  oen0  6726  oelim2  6735  nnaordi  6758  nnawordex  6777  pssnn  7224  fissuni  7307  dffi3  7331  cantnfle  7519  cantnflem1  7538  trcl  7557  r1sdom  7593  iscard2  7756  alephordi  7848  alephgeom  7856  cardaleph  7863  cardalephex  7864  ackbij2lem4  8015  cflm  8023  cfslbn  8040  cofsmo  8042  cfsmolem  8043  cfcoflem  8045  coftr  8046  alephsing  8049  fin23lem28  8113  fin23lem30  8115  fin23lem33  8118  fin1a2lem9  8181  axdc3lem2  8224  ttukeylem5  8287  fpwwe2lem5  8403  pwfseqlem4a  8430  pwfseqlem4  8431  wunex2  8507  inar1  8544  sstskm  8611  summolem2  12397  summo  12398  zsum  12399  sumz  12403  sumss  12405  fsumcvg3  12410  vdwlem1  13236  vdwlem12  13247  vdwlem13  13248  ramub2  13269  rami  13270  ramz2  13279  prdsval  13565  pwsle  13601  mrcuni  13733  isclat  14425  gsumpropd  14663  gsumress  14664  eqgfval  14875  sscntz  15012  resscntz  15017  lsmlub  15184  efgrelexlemb  15269  efgcpbllemb  15274  gsumval3a  15399  dmdprd  15446  dprdcntz  15453  subgdmdprd  15479  subrgpropd  15789  islss  15902  lsslss  15928  lsspropd  15984  lsmelpr  16054  lbspropd  16062  ltbval  16423  opsrval  16426  isbasisg  16902  tgval  16910  tgss3  16941  restbas  17106  tgrest  17107  restcld  17120  restopn2  17125  restntr  17129  cnpnei  17210  cncls2  17219  perfcls  17310  cmpsublem  17343  cmpsub  17344  cmpcld  17346  uncmp  17347  hauscmplem  17350  cmpfi  17352  nconsubb  17366  clscon  17373  hausllycmp  17437  1stckgenlem  17465  txbas  17479  ptbasfi  17493  txcnpi  17519  ptcnp  17533  txcmplem1  17552  txcmplem2  17553  xkococnlem  17570  qtopcld  17621  fbasssin  17744  fbssint  17746  fbun  17748  fbasrn  17792  filufint  17828  ufinffr  17837  ufildr  17839  elmopn  18201  neibl  18260  icccmplem1  18541  icccmplem2  18542  bndth  18671  isphtpc  18707  metcld  18946  bcthlem1  18961  bcth  18966  ovolfioo  19042  ovolficc  19043  elovolmr  19050  ovoliunlem3  19078  ovolicc2  19096  volsuplem  19127  dyadmax  19168  dyadmbllem  19169  dyadmbl  19170  sspval  21612  ubth  21765  orthin  22338  chssoc  22388  chsscon3  22392  chsscon1  22393  h1datom  22474  pjoml6i  22481  osum  22537  spansncv  22545  pjcjt2  22584  pjopyth  22612  hstel2  23112  hstle  23123  stj  23128  dmdbr5  23201  mdslmd1lem1  23218  atord  23281  chirredlem4  23286  atcvat4i  23290  mdsymlem2  23297  mdsymlem3  23298  mdsymlem8  23303  ssnnssfz  23549  gsumpropd2lem  23611  tpr2rico  23665  ustval  23707  trust  23732  cfilucfil  23802  sigaval  23958  issiga  23959  issgon  23971  sssigagen  23993  measiuns  24034  kur14  24350  cvmliftlem15  24432  ghomfo  24585  rtrclreclem.refl  24628  rtrclreclem.subset  24629  prodmolem2  24745  prodmo  24746  zprod  24747  prod1  24754  trpredtr  24974  dftrpred3g  24977  wfrlem9  25005  wfrlem12  25008  frrlem5e  25030  nofulllem1  25097  nofulllem2  25098  itgaddnclem2  25682  ivthALT  25765  isfne  25775  topfne  25797  neibastop3  25818  tailfb  25833  filnetlem1  25834  filnetlem4  25837  sstotbnd2  26004  sstotbnd  26005  sstotbnd3  26006  ssbnd  26018  cntotbnd  26026  cnpwstotbnd  26027  ismtyres  26038  heibor1lem  26039  heiborlem1  26041  heiborlem6  26046  heiborlem8  26048  exidreslem  26073  ismrc  26282  incssnn0  26292  nacsfix  26293  lsslinds  26807  hbt  26840  stoweidlem50  27305  stoweidlem57  27312  sbcrel  27487  isfrgra  27825  lshpcmp  29249  lsmsat  29269  lsmsatcv  29271  lfl1dim  29382  lfl1dim2N  29383  lkrss2N  29430  psubspset  30004  paddss  30105  psubclsetN  30196  dilfsetN  30412  dilsetN  30413  diaglbN  31316  dibglbN  31427  dihlspsnat  31594  dihglb2  31603  dochffval  31610  dochfval  31611  dochvalr  31618  dochord2N  31632  dochsncom  31643  dihjat1lem  31689  dvh4dimat  31699  dvh3dimatN  31700  dvh2dimatN  31701  dochexmidlem1  31721  lpolsetN  31743  lpolconN  31748  hdmaplkr  32177  hdmapoc  32195  hlhillcs  32222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator