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

Theorem eqsstrd 3298
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 3291 . 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 1647    C_ wss 3238
This theorem is referenced by:  eqsstr3d  3299  syl6eqss  3314  tfisi  4752  dmsnopss  5248  fvmptss  5716  fvmptss2  5726  fimacnv  5764  funressn  5819  suppssof1  6246  frxp  6353  riotassuni  6485  onfununi  6500  oawordeulem  6694  oewordri  6732  oeeui  6742  nnawordex  6777  oaabslem  6783  oaabs2  6785  omabslem  6786  omabs  6787  pw2f1olem  7109  fodomr  7155  fival  7313  dffi3  7331  ordtypelem7  7386  ordtypelem8  7387  wemapso2  7414  cantnflt2  7521  mapfien  7546  tcss  7576  tcel  7577  r1val1  7605  rankuni2b  7672  tcrank  7701  cardonle  7737  harval2  7777  carduniima  7870  ackbij1lem15  8007  ackbij2lem3  8014  ackbij2  8016  cfub  8022  cflecard  8026  cfflb  8032  fin23lem13  8105  isf32lem8  8133  itunitc1  8193  ttukeylem7  8289  fpwwe2lem9  8407  fpwwe2lem12  8410  wuncss  8514  wuncval2  8516  grur1a  8588  uzssz  10398  limsupgle  12158  limsupgre  12162  isercolllem2  12346  isercolllem3  12347  isercoll  12348  fsumss  12406  sadadd2lem  12858  sadadd3  12860  sadaddlem  12865  sadasslem  12869  sadeq  12871  prmreclem4  13174  prmreclem5  13175  1arith  13182  4sqlem19  13218  vdwmc2  13234  vdwlem1  13236  vdwlem12  13247  vdwlem13  13248  ramz2  13279  ramub1lem1  13281  ressbasss  13408  ressress  13413  imasaddfnlem  13640  imasaddflem  13642  imasvscafn  13649  imasvscaf  13651  imasless  13652  isohom  13884  ressffth  14022  acsfiindd  14490  acsmap2d  14492  dirref  14567  cntzrcl  15013  cntzssv  15014  sylow2alem2  15139  lsmssv  15164  lsmidm  15183  gsumzres  15404  dprdlub  15471  dprdf1  15478  dprdsn  15481  dprdcntz2  15483  dprd2dlem1  15486  dprd2da  15487  dmdprdsplit2lem  15490  ablfac1eu  15518  ablfaclem3  15532  lmhmlsp  16016  drnglpir  16215  issubassa2  16294  mplsubglem  16389  evlslem4  16455  znleval  16725  ntrss2  17011  lpsscls  17090  tgrest  17107  resttopon  17109  rest0  17117  restfpw  17127  ordtrest  17149  ordtrest2  17151  lmcnp  17249  tgcmp  17345  uncmp  17347  hauscmplem  17350  1stcfb  17388  2ndcdisj  17399  kgentopon  17450  kgencmp  17457  ptpjpre1  17483  xkouni  17511  xkoccn  17530  prdstopn  17539  txtube  17551  txcmplem2  17553  xkoptsub  17565  xkopt  17566  xkococnlem  17570  qtoprest  17625  imastopn  17628  kqdisj  17640  reghmph  17701  nrmhmph  17702  fbssfi  17745  trfilss  17797  trfg  17799  uzfbas  17806  elfm3  17858  alexsubALTlem3  17956  alexsubALT  17958  clsnsg  18005  tgpconcompeqg  18007  divstgphaus  18018  metequiv2  18269  prdsxmslem2  18288  iccntr  18540  icccmplem1  18541  metdstri  18569  pi1addf  18760  pi1addval  18761  pi1xfrcnvlem  18769  caubl  18948  caublcls  18949  relcmpcmet  18957  minveclem4  19011  hlhil  19022  ovolficcss  19044  ovolshftlem1  19083  ovolshft  19085  ovolscalem1  19087  ovolscalem2  19088  ovolsca  19089  uniioombllem2  19153  uniioombllem3a  19154  uniioombllem3  19155  uniioombllem4  19156  uniioombllem6  19158  dyadss  19164  opnmbllem  19171  i1fima2  19249  itgioo  19385  limcfval  19437  limcnlp  19443  dvfval  19462  dvbsss  19467  dvnres  19495  dvivth  19572  lhop  19578  dvcnvrelem1  19579  evlseu  19615  mpfrcl  19617  taylf  19955  pserdv  20023  rlimcnp2  20483  xrlimcnp  20485  jensen  20505  fsumharmonic  20528  ppisval  20564  chtlepsi  20668  chpval2  20680  chpub  20682  shsss  22326  chssoc  22509  speccl  22913  elnlfn  22942  mdsl0  23324  mdexchi  23349  atcvat3i  23410  dmdbr5ati  23436  funimass4f  23568  ofrn2  23577  xrofsup  23647  cnvordtrestixx  23787  pnfneige0  23812  cnextf  23823  cnextcn  23824  trust  23853  ustuqtop3  23867  metustfbas  23921  restmetu  23935  sigagenss  24118  imambfm  24196  dya2iocress  24208  dya2icoseg  24211  dya2iocucvr  24218  ballotlemro  24349  cvmliftmolem2  24537  cvmliftlem15  24553  cvmlift3lem6  24579  relexpfld  24706  rtrclreclem.min  24716  trpredmintr  25060  nobndlem8  25179  liness  25595  comppfsc  25899  neibastop2lem  25901  sdclem2  26044  sstotbnd2  26089  isbndx  26097  isbnd2  26098  ssbnd  26103  heiborlem3  26128  igenmin  26280  elrfi  26360  isnacs3  26376  mzpf  26405  mzpindd  26415  diophrw  26429  diophin  26443  eldiophss  26445  rmxyelqirr  26586  pw2f1ocnv  26721  aomclem6  26747  frlmplusgval  26820  frlmvscafval  26821  frlmsplit2  26834  f1lindf  26883  hbt  26925  itgocn  26960  rgspnmin  26967  en2other2  26973  f1omvdco2  26982  pmtrfrn  26991  symgsssg  26999  symggen  27002  psgnunilem1  27007  stoweidlem59  27399  bnj1262  28595  bnj1097  28763  bnj1452  28834  lsatlss  29245  lsmsat  29257  lsatfixedN  29258  lssats  29261  lpssat  29262  lssatle  29264  lssat  29265  lsatcvat3  29301  lkrlss  29344  pmapssat  30007  paddssat  30062  paddasslem17  30084  pmodlem2  30095  hlmod1i  30104  pl42lem4N  30230  diass  31291  diaintclN  31307  diassdvaN  31309  dia2dimlem10  31322  dia2dimlem13  31325  dibintclN  31416  cdlemn4a  31448  cdlemn5pre  31449  dihord5apre  31511  lclkrlem2e  31760  lclkrlem2p  31771  lclkrlem2v  31777  lclkrslem2  31787  lclkrs  31788  lcfrlem25  31816  lcfrlem35  31826  lcdvbasess  31843  mapdval2N  31879  mapdin  31911  mapdpglem8  31928  mapdpglem13  31933  baerlem3lem2  31959  mapdindp2  31970  hdmap11lem2  32094
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator