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

Theorem sseq1d 3513
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 3507 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1381    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  sseq12d  3515  eqsstrd  3520  snssg  4144  ssiun2s  4355  disjxiun  4430  treq  4532  funimass1  5647  feq1  5699  fvmptss  5945  fvimacnvi  5982  fvimacnvALT  5987  fnsuppresOLD  6112  knatar  6234  ovmptss  6862  fnsuppres  6925  imacosupp  6938  oaordi  7193  oaword2  7200  oawordeulem  7201  omword1  7220  oewordri  7239  oeordsuc  7241  nnaordi  7265  nnawordex  7284  ereq1  7316  elpm2r  7434  inficl  7883  fipwss  7887  dffi3  7889  hartogslem1  7965  inf3lema  8039  inf3lemd  8042  cantnfle  8088  cantnflem2  8107  cantnfleOLD  8118  trcl  8157  tcmin  8170  rankr1ai  8214  rankxplim  8295  scottex  8301  scott0  8302  scottexs  8303  scott0s  8304  karden  8311  cardne  8344  cardaleph  8468  ackbij2  8621  cflim2  8641  cfslb  8644  coftr  8651  fin23lem15  8712  fin23lem32  8722  fin23lem34  8724  fin23lem35  8725  fin23lem36  8726  fin23lem41  8730  isf32lem1  8731  itunitc1  8798  axdc3lem2  8829  ttukeylem1  8887  fpwwe2cbv  9006  fpwwe2lem2  9008  fpwwe2  9019  fpwwecbv  9020  fpwwelem  9021  canthwelem  9026  canthwe  9027  wunex2  9114  wuncval2  9123  eltsk2g  9127  tskpwss  9128  inar1  9151  grothpw  9202  grothpwex  9203  axgroth6  9204  grothac  9206  peano5uzti  10953  fsuppmapnn0fiub0  12073  lo1o1  13329  o1lo1  13334  o1lo12  13335  lo1eq  13365  rlimeq  13366  isercoll  13464  prmreclem4  14309  vdwmc  14368  vdwlem1  14371  vdwlem2  14372  vdwlem12  14382  vdwlem13  14383  ramval  14398  ramz2  14414  ramub1lem1  14416  isacs2  14922  isacs1i  14926  mreacs  14927  acsfn  14928  rescabs  15074  ipole  15657  ipodrsima  15664  isacs5  15671  symgsssg  16361  psgnunilem5  16388  sylow1  16492  efgval2  16611  efgsfo  16626  frgpuplem  16659  gsumzf1o  16786  gsumzoppg  16836  dprdcntz  16910  islbs2  17668  frlmssuvc1  18692  frlmssuvc2  18693  frlmssuvc1OLD  18694  frlmssuvc2OLD  18695  frlmsslsp  18696  frlmsslspOLD  18697  pptbas  19375  pnfnei  19587  mnfnei  19588  iscnp  19604  iscnp4  19630  cnntr  19642  cnconst2  19650  cnpresti  19655  cnprest  19656  isreg  19699  isnrm  19702  isnrm2  19725  perfcls  19732  isreg2  19744  hauscmplem  19772  1stcfb  19812  1stcelcls  19828  1stccnp  19829  txbas  19934  ptbasfi  19948  xkoopn  19956  xkoccn  19986  txcnp  19987  ptcnplem  19988  txdis  19999  txdis1cn  20002  txtube  20007  txkgen  20019  xkohaus  20020  xkoptsub  20021  xkoco1cn  20024  xkoco2cn  20025  xkococnlem  20026  xkococn  20027  xkoinjcn  20054  kqreglem1  20108  kqreglem2  20109  kqnrmlem1  20110  kqnrmlem2  20111  reghmph  20160  nrmhmph  20161  trfil2  20254  ufileu  20286  elfm  20314  elfm2  20315  elfm3  20317  imaelfm  20318  rnelfm  20320  fmfnfmlem2  20322  fmfnfmlem4  20324  fmco  20328  elflim2  20331  flffbas  20362  lmflf  20372  txflf  20373  fclscf  20392  flimfnfcls  20395  cnextcn  20433  symgtgp  20466  ghmcnp  20479  qustgplem  20485  eltsms  20497  ustval  20571  ust0  20588  trust  20598  utoptop  20603  restutop  20606  restutopopn  20607  utopsnneiplem  20616  ucncn  20654  fmucnd  20661  cfilufg  20662  trcfilu  20663  neipcfilu  20665  blssps  20793  blss  20794  ssblex  20797  blin2  20798  metss2  20881  metrest  20893  metcnp3  20909  metustexhalfOLD  20932  metustexhalf  20933  metustblOLD  20949  metustbl  20950  metutopOLD  20951  psmetutop  20952  xrsmopn  21183  recld2  21185  icccmplem1  21193  icccmplem2  21194  icccmp  21196  reconnlem2  21198  lebnumlem3  21329  lebnum  21330  xlebnum  21331  lebnumii  21332  nmhmcn  21469  cfilfval  21569  caubl  21612  caublcls  21613  bcthlem1  21629  bcth  21634  ovolfiniun  21778  ovoliunlem3  21781  ovoliun  21782  ovoliun2  21783  ovoliunnul  21784  voliunlem3  21828  dyadmax  21873  dyadmbllem  21874  dyadmbl  21875  opnmbllem  21876  ellimc2  22147  limcnlp  22148  ellimc3  22149  limcflf  22151  limciun  22164  cpnord  22204  lhop  22283  xrlimcnp  23163  cvxcl  23179  dchrval  23374  frgraunss  24860  frgra1v  24863  frgra2v  24864  frgra3vlem1  24865  frgra3vlem2  24866  frgra3v  24867  4cycl2vnunb  24882  n4cyclfrgra  24883  isssp  25502  ubthlem1  25651  shmodi  26173  chsupid  26195  chsscon3  26283  spansncvi  26435  mdslmd1lem3  27111  mdslmd1lem4  27112  mdsymlem5  27191  dmdbr5ati  27206  dmdbr6ati  27207  dmdbr7ati  27208  ssiun2sf  27292  fpwrelmapffslem  27420  txomap  27703  locfinreflem  27709  tpr2rico  27760  pnfneige0  27799  rrhre  27865  dya2icoseg2  28115  omsfval  28131  eulerpartlemt0  28174  eulerpartgbij  28177  eulerpartlemr  28179  eulerpartlemgs2  28185  eulerpartlemn  28186  eulerpart  28187  kur14  28526  cvmliftlem15  28609  cvmlift2lem12  28625  cvmlift2lem13  28626  mclsval  28789  mclsax  28795  mclsppslem  28809  relexpdm  28924  relexprn  28925  rtrclreclem.min  28936  dfrtrcl2  28937  dfpo2  29152  preddowncl  29244  trpredlem1  29278  trpredmintr  29282  wrecseq123  29305  wfrlem1  29311  wfrlem3  29313  wfrlem9  29319  wfrlem15  29325  frrlem1  29355  frrlem4  29358  frrlem5e  29363  nobndup  29428  nobnddown  29429  nofulllem5  29434  opnmbllem0  30018  mblfinlem1  30019  mblfinlem2  30020  mblfinlem3  30021  ovoliunnfl  30024  ex-ovoliunnfl  30025  voliunnfl  30026  opnrebl  30106  opnrebl2  30107  ivthALT  30121  neibastop2lem  30146  fnemeet1  30152  filnetlem1  30164  filnetlem4  30167  totbndbnd  30253  heibor1lem  30273  heiborlem10  30284  scottexf  30544  scott0f  30545  ismrcd1  30598  nacsfix  30612  setindtr  30934  hbtlem6  31046  icccncfext  31593  fourierdlem41  31815  dfrngc2  32499  bnj517  33650  bnj1014  33725  bnj1015  33726  bnj1123  33749  bnj1125  33755  bnj1450  33813  bnj1452  33815  lcv1  34468  lfl1dim  34548  lfl1dim2N  34549  paddasslem17  35262  dihglblem6  36769  dochvalr  36786  dochord3  36801  lpolconN  36916  lcfls1lem  36963  mapdffval  37055  mapdfval  37056  mapdsn2  37071  mapd0  37094  lspindp5  37199  mapdh8ab  37206
  Copyright terms: Public domain W3C validator