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

Theorem eqsstrd 3212
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstrd.1  |-  ( ph  ->  A  =  B )
eqsstrd.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
eqsstrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem eqsstrd
StepHypRef Expression
1 eqsstrd.2 . 2  |-  ( ph  ->  B  C_  C )
2 eqsstrd.1 . . 3  |-  ( ph  ->  A  =  B )
32sseq1d 3205 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 223 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  eqsstr3d  3213  syl6eqss  3228  tfisi  4649  dmsnopss  5145  fvmptss  5609  fvmptss2  5619  fimacnv  5657  funressn  5706  suppssof1  6119  frxp  6225  riotassuni  6343  onfununi  6358  oawordeulem  6552  oewordri  6590  oeeui  6600  nnawordex  6635  oaabslem  6641  oaabs2  6643  omabslem  6644  omabs  6645  pw2f1olem  6966  fodomr  7012  fival  7166  dffi3  7184  ordtypelem7  7239  ordtypelem8  7240  wemapso2  7267  cantnflt2  7374  mapfien  7399  tcss  7429  tcel  7430  r1val1  7458  rankuni2b  7525  tcrank  7554  cardonle  7590  harval2  7630  carduniima  7723  ackbij1lem15  7860  ackbij2lem3  7867  ackbij2  7869  cfub  7875  cflecard  7879  cfflb  7885  fin23lem13  7958  isf32lem8  7986  itunitc1  8046  ttukeylem7  8142  fpwwe2lem9  8260  fpwwe2lem12  8263  wuncss  8367  wuncval2  8369  grur1a  8441  uzssz  10247  limsupgle  11951  limsupgre  11955  isercolllem2  12139  isercolllem3  12140  isercoll  12141  fsumss  12198  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  prmreclem4  12966  prmreclem5  12967  1arith  12974  4sqlem19  13010  vdwmc2  13026  vdwlem1  13028  vdwlem12  13039  vdwlem13  13040  ramz2  13071  ramub1lem1  13073  ressbasss  13200  ressress  13205  imasaddfnlem  13430  imasaddflem  13432  imasvscafn  13439  imasvscaf  13441  imasless  13442  isohom  13674  ressffth  13812  acsfiindd  14280  acsmap2d  14282  dirref  14357  cntzrcl  14803  cntzssv  14804  sylow2alem2  14929  lsmssv  14954  lsmidm  14973  gsumzres  15194  dprdlub  15261  dprdf1  15268  dprdsn  15271  dprdcntz2  15273  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  ablfac1eu  15308  ablfaclem3  15322  lmhmlsp  15806  drnglpir  16005  issubassa2  16084  mplsubglem  16179  evlslem4  16245  znleval  16508  ntrss2  16794  lpsscls  16873  tgrest  16890  resttopon  16892  rest0  16900  restfpw  16910  ordtrest  16932  ordtrest2  16934  lmcnp  17032  tgcmp  17128  uncmp  17130  hauscmplem  17133  1stcfb  17171  2ndcdisj  17182  kgentopon  17233  kgencmp  17240  ptpjpre1  17266  xkouni  17294  xkoccn  17313  prdstopn  17322  txtube  17334  txcmplem2  17336  xkoptsub  17348  xkopt  17349  xkococnlem  17353  qtoprest  17408  imastopn  17411  kqdisj  17423  reghmph  17484  nrmhmph  17485  fbssfi  17532  trfilss  17584  trfg  17586  uzfbas  17593  elfm3  17645  alexsubALTlem3  17743  alexsubALT  17745  clsnsg  17792  tgpconcompeqg  17794  divstgphaus  17805  metequiv2  18056  prdsxmslem2  18075  iccntr  18326  icccmplem1  18327  metdstri  18355  pi1addf  18545  pi1addval  18546  pi1xfrcnvlem  18554  caubl  18733  caublcls  18734  relcmpcmet  18742  minveclem4  18796  hlhil  18807  ovolficcss  18829  ovolshftlem1  18868  ovolshft  18870  ovolscalem1  18872  ovolscalem2  18873  ovolsca  18874  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  dyadss  18949  opnmbllem  18956  i1fima2  19034  itgioo  19170  limcfval  19222  limcnlp  19228  dvfval  19247  dvbsss  19252  dvnres  19280  dvivth  19357  lhop  19363  dvcnvrelem1  19364  evlseu  19400  mpfrcl  19402  taylf  19740  pserdv  19805  rlimcnp2  20261  xrlimcnp  20263  jensen  20283  fsumharmonic  20305  ppisval  20341  chtlepsi  20445  chpval2  20457  chpub  20459  shsss  21892  chssoc  22075  speccl  22479  elnlfn  22508  mdsl0  22890  mdexchi  22915  atcvat3i  22976  dmdbr5ati  23002  funimass4f  23042  ballotlemro  23081  ofrn2  23207  xrofsup  23255  cnvordtrestixx  23297  pnfneige0  23374  sigagenss  23510  imambfm  23567  dya2iocress  23577  dya2iocseg  23579  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift3lem6  23855  relexpfld  24034  rtrclreclem.min  24044  trpredmintr  24234  nobndlem8  24353  liness  24768  rnintintrn  25126  preoref12  25228  flfnei2  25577  dualalg  25782  tartarmap  25888  cardtar  25904  prismorcsetlem  25912  prismorcset  25914  morexcmp  25967  cmppar  25973  smbkle  26043  lineval12a  26084  rayline  26156  comppfsc  26307  neibastop2lem  26309  sdclem2  26452  sstotbnd2  26498  isbndx  26506  isbnd2  26507  ssbnd  26512  heiborlem3  26537  igenmin  26689  elrfi  26769  isnacs3  26785  mzpf  26814  mzpindd  26824  diophrw  26838  diophin  26852  eldiophss  26854  rmxyelqirr  26995  pw2f1ocnv  27130  aomclem6  27156  frlmplusgval  27229  frlmvscafval  27230  frlmsplit2  27243  f1lindf  27292  hbt  27334  itgocn  27369  rgspnmin  27376  en2other2  27382  f1omvdco2  27391  pmtrfrn  27400  symgsssg  27408  symggen  27411  psgnunilem1  27416  stoweidlem59  27808  bnj1262  28843  bnj1097  29011  bnj1452  29082  lsatlss  29186  lsmsat  29198  lsatfixedN  29199  lssats  29202  lpssat  29203  lssatle  29205  lssat  29206  lsatcvat3  29242  lkrlss  29285  pmapssat  29948  paddssat  30003  paddasslem17  30025  pmodlem2  30036  hlmod1i  30045  pl42lem4N  30171  diass  31232  diaintclN  31248  diassdvaN  31250  dia2dimlem10  31263  dia2dimlem13  31266  dibintclN  31357  cdlemn4a  31389  cdlemn5pre  31390  dihord5apre  31452  lclkrlem2e  31701  lclkrlem2p  31712  lclkrlem2v  31718  lclkrslem2  31728  lclkrs  31729  lcfrlem25  31757  lcfrlem35  31767  lcdvbasess  31784  mapdval2N  31820  mapdin  31852  mapdpglem8  31869  mapdpglem13  31874  baerlem3lem2  31900  mapdindp2  31911  hdmap11lem2  32035
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