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

Theorem sseq2d 3206
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 3200 . 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 1623    C_ wss 3152
This theorem is referenced by:  sseq12d  3207  sseqtrd  3214  funimass2  5326  fnco  5352  fnssresb  5356  fnimaeq0  5365  foimacnv  5490  fvelimab  5578  ssimaexg  5585  knatar  5857  onfununi  6358  oaordi  6544  oawordeulem  6552  oaass  6559  odi  6577  omass  6578  oen0  6584  oelim2  6593  nnaordi  6616  nnawordex  6635  pssnn  7081  fissuni  7160  dffi3  7184  cantnfle  7372  cantnflem1  7391  trcl  7410  r1sdom  7446  iscard2  7609  alephordi  7701  alephgeom  7709  cardaleph  7716  cardalephex  7717  ackbij2lem4  7868  cflm  7876  cfslbn  7893  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  coftr  7899  alephsing  7902  fin23lem28  7966  fin23lem30  7968  fin23lem33  7971  fin1a2lem9  8034  axdc3lem2  8077  ttukeylem5  8140  fpwwe2lem5  8256  pwfseqlem4a  8283  pwfseqlem4  8284  wunex2  8360  inar1  8397  sstskm  8464  summolem2  12189  summo  12190  zsum  12191  sumz  12195  sumss  12197  fsumcvg3  12202  vdwlem1  13028  vdwlem12  13039  vdwlem13  13040  ramub2  13061  rami  13062  ramz2  13071  prdsval  13355  pwsle  13391  mrcuni  13523  isclat  14215  gsumpropd  14453  gsumress  14454  eqgfval  14665  sscntz  14802  resscntz  14807  lsmlub  14974  efgrelexlemb  15059  efgcpbllemb  15064  gsumval3a  15189  dmdprd  15236  dprdcntz  15243  subgdmdprd  15269  subrgpropd  15579  islss  15692  lsslss  15718  lsspropd  15774  lsmelpr  15844  lbspropd  15852  ltbval  16213  opsrval  16216  isbasisg  16685  tgval  16693  tgss3  16724  restbas  16889  tgrest  16890  restcld  16903  restopn2  16908  restntr  16912  cnpnei  16993  cncls2  17002  perfcls  17093  cmpsublem  17126  cmpsub  17127  cmpcld  17129  uncmp  17130  hauscmplem  17133  cmpfi  17135  nconsubb  17149  clscon  17156  hausllycmp  17220  1stckgenlem  17248  txbas  17262  ptbasfi  17276  txcnpi  17302  ptcnp  17316  txcmplem1  17335  txcmplem2  17336  xkococnlem  17353  qtopcld  17404  fbasssin  17531  fbssint  17533  fbun  17535  fbasrn  17579  filufint  17615  ufinffr  17624  ufildr  17626  elmopn  17988  neibl  18047  icccmplem1  18327  icccmplem2  18328  bndth  18456  isphtpc  18492  metcld  18731  bcthlem1  18746  bcth  18751  ovolfioo  18827  ovolficc  18828  elovolmr  18835  ovoliunlem3  18863  ovolicc2  18881  volsuplem  18912  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  sspval  21299  ubth  21452  orthin  22025  chssoc  22075  chsscon3  22079  chsscon1  22080  h1datom  22161  pjoml6i  22168  osum  22224  spansncv  22232  pjcjt2  22271  pjopyth  22299  hstel2  22799  hstle  22810  stj  22815  dmdbr5  22888  mdslmd1lem1  22905  atord  22968  chirredlem4  22973  atcvat4i  22977  mdsymlem2  22984  mdsymlem3  22985  mdsymlem8  22990  ssnnssfz  23277  tpr2rico  23296  gsumpropd2lem  23379  sigaval  23471  issiga  23472  issgon  23484  sssigagen  23506  measiuns  23544  kur14  23747  cvmliftlem15  23829  ghomfo  23998  rtrclreclem.refl  24041  rtrclreclem.subset  24042  trpredtr  24233  dftrpred3g  24236  wfrlem9  24264  wfrlem12  24267  frrlem5e  24289  nofulllem1  24356  nofulllem2  24357  inpc  25277  basexre  25522  isalg  25721  ivthALT  26258  isfne  26268  topfne  26290  neibastop3  26311  tailfb  26326  filnetlem1  26327  filnetlem4  26330  sstotbnd2  26498  sstotbnd  26499  sstotbnd3  26500  ssbnd  26512  cntotbnd  26520  cnpwstotbnd  26521  ismtyres  26532  heibor1lem  26533  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  exidreslem  26567  ismrc  26776  incssnn0  26786  nacsfix  26787  lsslinds  27301  hbt  27334  stoweidlem50  27799  stoweidlem57  27806  sbcrel  27979  isfrgra  28171  lshpcmp  29178  lsmsat  29198  lsmsatcv  29200  lfl1dim  29311  lfl1dim2N  29312  lkrss2N  29359  psubspset  29933  paddss  30034  psubclsetN  30125  dilfsetN  30341  dilsetN  30342  diaglbN  31245  dibglbN  31356  dihlspsnat  31523  dihglb2  31532  dochffval  31539  dochfval  31540  dochvalr  31547  dochord2N  31561  dochsncom  31572  dihjat1lem  31618  dvh4dimat  31628  dvh3dimatN  31629  dvh2dimatN  31630  dochexmidlem1  31650  lpolsetN  31672  lpolconN  31677  hdmaplkr  32106  hdmapoc  32124  hlhillcs  32151
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator