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

Theorem sseq1d 3481
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 3475 . 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 1370    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  sseq12d  3483  eqsstrd  3488  snssg  4105  ssiun2s  4312  disjxiun  4387  treq  4489  funimass1  5589  feq1  5640  fvmptss  5881  fvimacnvi  5916  fvimacnvALT  5921  fnsuppresOLD  6037  knatar  6147  ovmptss  6754  fnsuppres  6816  imacosupp  6829  oaordi  7085  oaword2  7092  oawordeulem  7093  omword1  7112  oewordri  7131  oeordsuc  7133  nnaordi  7157  nnawordex  7176  ereq1  7208  elpm2r  7330  inficl  7776  fipwss  7780  dffi3  7782  hartogslem1  7857  inf3lema  7931  inf3lemd  7934  cantnfle  7980  cantnflem2  7999  cantnfleOLD  8010  trcl  8049  tcmin  8062  rankr1ai  8106  rankxplim  8187  scottex  8193  scott0  8194  scottexs  8195  scott0s  8196  karden  8203  cardne  8236  cardaleph  8360  ackbij2  8513  cflim2  8533  cfslb  8536  coftr  8543  fin23lem15  8604  fin23lem32  8614  fin23lem34  8616  fin23lem35  8617  fin23lem36  8618  fin23lem41  8622  isf32lem1  8623  itunitc1  8690  axdc3lem2  8721  ttukeylem1  8779  fpwwe2cbv  8898  fpwwe2lem2  8900  fpwwe2  8911  fpwwecbv  8912  fpwwelem  8913  canthwelem  8918  canthwe  8919  wunex2  9006  wuncval2  9015  eltsk2g  9019  tskpwss  9020  inar1  9043  grothpw  9094  grothpwex  9095  axgroth6  9096  grothac  9098  peano5uzti  10832  lo1o1  13112  o1lo1  13117  o1lo12  13118  lo1eq  13148  rlimeq  13149  isercoll  13247  prmreclem4  14082  vdwmc  14141  vdwlem1  14144  vdwlem2  14145  vdwlem12  14155  vdwlem13  14156  ramval  14171  ramz2  14187  ramub1lem1  14189  isacs2  14693  isacs1i  14697  mreacs  14698  acsfn  14699  rescabs  14848  ipole  15430  ipodrsima  15437  isacs5  15444  symgsssg  16075  psgnunilem5  16102  sylow1  16206  efgval2  16325  efgsfo  16340  frgpuplem  16373  gsumzf1o  16495  gsumzmhm  16535  gsumzoppg  16545  dprdcntz  16597  islbs2  17341  frlmssuvc1  18328  frlmssuvc2  18329  frlmssuvc1OLD  18330  frlmssuvc2OLD  18331  frlmsslsp  18332  frlmsslspOLD  18333  pptbas  18728  pnfnei  18940  mnfnei  18941  iscnp  18957  iscnp4  18983  cnntr  18995  cnconst2  19003  cnpresti  19008  cnprest  19009  isreg  19052  isnrm  19055  isnrm2  19078  perfcls  19085  isreg2  19097  hauscmplem  19125  1stcfb  19165  1stcelcls  19181  1stccnp  19182  txbas  19256  ptbasfi  19270  xkoopn  19278  xkoccn  19308  txcnp  19309  ptcnplem  19310  txdis  19321  txdis1cn  19324  txtube  19329  txkgen  19341  xkohaus  19342  xkoptsub  19343  xkoco1cn  19346  xkoco2cn  19347  xkococnlem  19348  xkococn  19349  xkoinjcn  19376  kqreglem1  19430  kqreglem2  19431  kqnrmlem1  19432  kqnrmlem2  19433  reghmph  19482  nrmhmph  19483  trfil2  19576  ufileu  19608  elfm  19636  elfm2  19637  elfm3  19639  imaelfm  19640  rnelfm  19642  fmfnfmlem2  19644  fmfnfmlem4  19646  fmco  19650  elflim2  19653  flffbas  19684  lmflf  19694  txflf  19695  fclscf  19714  flimfnfcls  19717  cnextcn  19755  symgtgp  19788  ghmcnp  19801  divstgplem  19807  eltsms  19819  ustval  19893  ust0  19910  trust  19920  utoptop  19925  restutop  19928  restutopopn  19929  utopsnneiplem  19938  ucncn  19976  fmucnd  19983  cfilufg  19984  trcfilu  19985  neipcfilu  19987  blssps  20115  blss  20116  ssblex  20119  blin2  20120  metss2  20203  metrest  20215  metcnp3  20231  metustexhalfOLD  20254  metustexhalf  20255  metustblOLD  20271  metustbl  20272  metutopOLD  20273  psmetutop  20274  xrsmopn  20505  recld2  20507  icccmplem1  20515  icccmplem2  20516  icccmp  20518  reconnlem2  20520  lebnumlem3  20651  lebnum  20652  xlebnum  20653  lebnumii  20654  nmhmcn  20791  cfilfval  20891  caubl  20934  caublcls  20935  bcthlem1  20951  bcth  20956  ovolfiniun  21100  ovoliunlem3  21103  ovoliun  21104  ovoliun2  21105  ovoliunnul  21106  voliunlem3  21149  dyadmax  21194  dyadmbllem  21195  dyadmbl  21196  opnmbllem  21197  ellimc2  21468  limcnlp  21469  ellimc3  21470  limcflf  21472  limciun  21485  cpnord  21525  lhop  21604  xrlimcnp  22478  cvxcl  22494  dchrval  22689  isssp  24257  ubthlem1  24406  shmodi  24928  chsupid  24950  chsscon3  25038  spansncvi  25190  mdslmd1lem3  25866  mdslmd1lem4  25867  mdsymlem5  25946  dmdbr5ati  25961  dmdbr6ati  25962  dmdbr7ati  25963  ssiun2sf  26044  fpwrelmapffslem  26166  tpr2rico  26476  pnfneige0  26515  rrhre  26581  dya2icoseg2  26827  omsfval  26843  eulerpartlemt0  26886  eulerpartgbij  26889  eulerpartlemr  26891  eulerpartlemgs2  26897  eulerpartlemn  26898  eulerpart  26899  kur14  27238  cvmliftlem15  27321  cvmlift2lem12  27337  cvmlift2lem13  27338  relexpdm  27471  relexprn  27472  rtrclreclem.min  27483  dfrtrcl2  27484  dfpo2  27699  preddowncl  27791  trpredlem1  27825  trpredmintr  27829  wrecseq123  27852  wfrlem1  27858  wfrlem3  27860  wfrlem9  27866  wfrlem15  27872  frrlem1  27902  frrlem4  27905  frrlem5e  27910  nobndup  27975  nobnddown  27976  nofulllem5  27981  opnmbllem0  28565  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  ovoliunnfl  28571  ex-ovoliunnfl  28572  voliunnfl  28573  opnrebl  28653  opnrebl2  28654  ivthALT  28668  neibastop2lem  28719  fnemeet1  28725  filnetlem1  28737  filnetlem4  28740  totbndbnd  28826  heibor1lem  28846  heiborlem10  28857  scottexf  29118  scott0f  29119  ismrcd1  29172  nacsfix  29186  setindtr  29511  hbtlem6  29623  frgraunss  30725  frgra1v  30728  frgra2v  30729  frgra3vlem1  30730  frgra3vlem2  30731  frgra3v  30732  4cycl2vnunb  30747  n4cyclfrgra  30748  fsuppmapnn0fiub0  30939  bnj517  32178  bnj1014  32253  bnj1015  32254  bnj1123  32277  bnj1125  32283  bnj1450  32341  bnj1452  32343  lcv1  32992  lfl1dim  33072  lfl1dim2N  33073  paddasslem17  33786  dihglblem6  35291  dochvalr  35308  dochord3  35323  lpolconN  35438  lcfls1lem  35485  mapdffval  35577  mapdfval  35578  mapdsn2  35593  mapd0  35616  lspindp5  35721  mapdh8ab  35728
  Copyright terms: Public domain W3C validator