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

Theorem sseq1d 3459
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
sseq1d  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )

Proof of Theorem sseq1d
StepHypRef Expression
1 sseq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sseq1 3453 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 17 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1444    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418
This theorem is referenced by:  sseq12d  3461  eqsstrd  3466  snssg  4105  ssiun2s  4322  disjxiun  4399  treq  4503  preddowncl  5407  funimass1  5656  feq1  5710  fvmptss  5958  fvimacnvi  5996  fvimacnvALT  6001  knatar  6248  ovmptss  6877  fnsuppres  6942  imacosupp  6955  wrecseq123  7029  wfrlem1  7035  wfrlem3  7037  wfrdmcl  7044  wfrlem15  7050  wfrlem17  7052  dfrecs3  7091  oaordi  7247  oaword2  7254  oawordeulem  7255  omword1  7274  oewordri  7293  oeordsuc  7295  nnaordi  7319  nnawordex  7338  ereq1  7370  elpm2r  7489  inficl  7939  fipwss  7943  dffi3  7945  hartogslem1  8057  inf3lema  8129  inf3lemd  8132  cantnfle  8176  cantnflem2  8195  trcl  8212  tcmin  8225  rankr1ai  8269  rankxplim  8350  scottex  8356  scott0  8357  scottexs  8358  scott0s  8359  karden  8366  cardne  8399  cardaleph  8520  ackbij2  8673  cflim2  8693  cfslb  8696  coftr  8703  fin23lem15  8764  fin23lem32  8774  fin23lem34  8776  fin23lem35  8777  fin23lem36  8778  fin23lem41  8782  isf32lem1  8783  itunitc1  8850  axdc3lem2  8881  ttukeylem1  8939  fpwwe2cbv  9055  fpwwe2lem2  9057  fpwwe2  9068  fpwwecbv  9069  fpwwelem  9070  canthwelem  9075  canthwe  9076  wunex2  9163  wuncval2  9172  eltsk2g  9176  tskpwss  9177  inar1  9200  grothpw  9251  grothpwex  9252  axgroth6  9253  grothac  9255  peano5uzti  11025  fsuppmapnn0fiub0  12205  relexpnndm  13104  rtrclreclem4  13124  dfrtrcl2  13125  lo1o1  13596  o1lo1  13601  o1lo12  13602  lo1eq  13632  rlimeq  13633  isercoll  13731  prmreclem4  14863  vdwmc  14928  vdwlem1  14931  vdwlem2  14932  vdwlem12  14942  vdwlem13  14943  ramval  14960  ramvalOLD  14961  ramz2  14982  ramub1lem1  14984  isacs2  15559  isacs1i  15563  mreacs  15564  acsfn  15565  rescabs  15738  ipole  16404  ipodrsima  16411  isacs5  16418  symgsssg  17108  psgnunilem5  17135  sylow1  17255  efgval2  17374  efgsfo  17389  frgpuplem  17422  gsumzf1o  17546  gsumzoppg  17577  dprdcntz  17640  islbs2  18377  frlmssuvc1  19352  frlmssuvc2  19353  frlmsslsp  19354  pptbas  20023  pnfnei  20236  mnfnei  20237  iscnp  20253  iscnp4  20279  cnntr  20291  cnconst2  20299  cnpresti  20304  cnprest  20305  isreg  20348  isnrm  20351  isnrm2  20374  perfcls  20381  isreg2  20393  hauscmplem  20421  1stcfb  20460  1stcelcls  20476  1stccnp  20477  txbas  20582  ptbasfi  20596  xkoopn  20604  xkoccn  20634  txcnp  20635  ptcnplem  20636  txdis  20647  txdis1cn  20650  txtube  20655  txkgen  20667  xkohaus  20668  xkoptsub  20669  xkoco1cn  20672  xkoco2cn  20673  xkococnlem  20674  xkococn  20675  xkoinjcn  20702  kqreglem1  20756  kqreglem2  20757  kqnrmlem1  20758  kqnrmlem2  20759  reghmph  20808  nrmhmph  20809  trfil2  20902  ufileu  20934  elfm  20962  elfm2  20963  elfm3  20965  imaelfm  20966  rnelfm  20968  fmfnfmlem2  20970  fmfnfmlem4  20972  fmco  20976  elflim2  20979  flffbas  21010  lmflf  21020  txflf  21021  fclscf  21040  flimfnfcls  21043  cnextcn  21082  symgtgp  21116  ghmcnp  21129  qustgplem  21135  eltsms  21147  ustval  21217  ust0  21234  trust  21244  utoptop  21249  restutop  21252  restutopopn  21253  utopsnneiplem  21262  ucncn  21300  fmucnd  21307  cfilufg  21308  trcfilu  21309  neipcfilu  21311  blssps  21439  blss  21440  ssblex  21443  blin2  21444  metss2  21527  metrest  21539  metcnp3  21555  metustexhalf  21571  metustbl  21581  psmetutop  21582  xrsmopn  21830  recld2  21832  icccmplem1  21840  icccmplem2  21841  icccmp  21843  reconnlem2  21845  lebnumlem3  21991  lebnumlem3OLD  21994  lebnum  21995  xlebnum  21996  lebnumii  21997  nmhmcn  22134  cfilfval  22234  caubl  22277  caublcls  22278  bcthlem1  22292  bcth  22297  ovolfiniun  22454  ovoliunlem3  22457  ovoliun  22458  ovoliun2  22459  ovoliunnul  22460  voliunlem3  22505  dyadmax  22556  dyadmbllem  22557  dyadmbl  22558  opnmbllem  22559  ellimc2  22832  limcnlp  22833  ellimc3  22834  limcflf  22836  limciun  22849  cpnord  22889  lhop  22968  xrlimcnp  23894  cvxcl  23910  dchrval  24162  frgraunss  25723  frgra1v  25726  frgra2v  25727  frgra3vlem1  25728  frgra3vlem2  25729  frgra3v  25730  4cycl2vnunb  25745  n4cyclfrgra  25746  isssp  26363  ubthlem1  26512  shmodi  27043  chsupid  27065  chsscon3  27153  spansncvi  27305  mdslmd1lem3  27980  mdslmd1lem4  27981  mdsymlem5  28060  dmdbr5ati  28075  dmdbr6ati  28076  dmdbr7ati  28077  ssiun2sf  28174  fpwrelmapffslem  28317  txomap  28661  locfinreflem  28667  tpr2rico  28718  pnfneige0  28757  rrhre  28825  dya2icoseg2  29100  omsfval  29118  omsfvalOLD  29122  eulerpartlemt0  29202  eulerpartgbij  29205  eulerpartlemr  29207  eulerpartlemgs2  29213  eulerpartlemn  29214  eulerpart  29215  bnj517  29696  bnj1014  29771  bnj1015  29772  bnj1123  29795  bnj1125  29801  bnj1450  29859  bnj1452  29861  kur14  29939  cvmliftlem15  30021  cvmlift2lem12  30037  cvmlift2lem13  30038  mclsval  30201  mclsax  30207  mclsppslem  30221  dfpo2  30395  trpredlem1  30468  trpredmintr  30472  frrlem1  30514  frrlem4  30517  frrlem5e  30522  nobndup  30589  nobnddown  30590  nofulllem5  30595  opnrebl  30976  opnrebl2  30977  ivthALT  30991  neibastop2lem  31016  fnemeet1  31022  filnetlem1  31034  filnetlem4  31037  csbwrecsg  31728  ptrecube  31940  poimirlem32  31972  opnmbllem0  31976  mblfinlem1  31977  mblfinlem2  31978  mblfinlem3  31979  ovoliunnfl  31982  ex-ovoliunnfl  31983  voliunnfl  31984  totbndbnd  32121  heibor1lem  32141  heiborlem10  32152  scottexf  32411  scott0f  32412  lcv1  32607  lfl1dim  32687  lfl1dim2N  32688  paddasslem17  33401  dihglblem6  34908  dochvalr  34925  dochord3  34940  lpolconN  35055  lcfls1lem  35102  mapdffval  35194  mapdfval  35195  mapdsn2  35210  mapd0  35233  lspindp5  35338  mapdh8ab  35345  ismrcd1  35540  nacsfix  35554  setindtr  35879  hbtlem6  35988  clcnvlem  36230  iunrelexpmin1  36300  iunrelexpmin2  36304  relexp0a  36308  cotrcltrcl  36317  trclimalb2  36318  cotrclrcl  36334  sbcheg  36374  ssnnf1octb  37470  icccncfext  37765  fourierdlem41  38011  hoidmvlelem3  38419  hoidmvle  38422  opnvonmbllem1  38454  opnvonmbl  38456  iunopeqop  39005  ausgrumgri  39254  ausgrusgri  39255  nbgrval  39406  nbgrel  39410  nbumgrvtx  39414  nbgrnself  39429  uvtxael1  39468  1wlkvtxiedg  39638  1wlk1walk  39648  dfrngc2  40027
  Copyright terms: Public domain W3C validator