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

Theorem eqsstrd 3384
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 3377 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 225 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3322
This theorem is referenced by:  eqsstr3d  3385  syl6eqss  3400  tfisi  4841  suppssof1  6349  riotassuni  6591  onfununi  6606  oawordeulem  6800  oeeui  6848  nnawordex  6883  oaabslem  6889  oaabs2  6891  omabslem  6892  omabs  6893  pw2f1olem  7215  fodomr  7261  fival  7420  dffi3  7439  ordtypelem7  7496  ordtypelem8  7497  wemapso2  7524  cantnflt2  7631  mapfien  7656  tcss  7686  tcel  7687  r1val1  7715  rankuni2b  7782  tcrank  7813  cardonle  7849  harval2  7889  carduniima  7982  ackbij2  8128  cfub  8134  cflecard  8138  cfflb  8144  isf32lem8  8245  itunitc1  8305  ttukeylem7  8400  fpwwe2lem9  8518  wuncss  8625  wuncval2  8627  grur1a  8699  limsupgre  12280  isercolllem3  12465  4sqlem19  13336  vdwlem1  13354  vdwlem12  13365  ramub1lem1  13399  ressress  13531  imasaddfnlem  13758  imasaddflem  13760  imasvscafn  13767  imasvscaf  13769  imasless  13770  isohom  14002  ressffth  14140  acsfiindd  14608  acsmap2d  14610  dirref  14685  sylow2alem2  15257  lsmssv  15282  lsmidm  15301  gsumzres  15522  dprdlub  15589  dprdf1  15596  dprdsn  15599  dprdcntz2  15601  dprd2dlem1  15604  dprd2da  15605  dmdprdsplit2lem  15608  ablfac1eu  15636  drnglpir  16329  issubassa2  16408  evlslem4  16569  znleval  16840  lpsscls  17210  tgrest  17228  resttopon  17230  rest0  17238  restfpw  17248  ordtrest  17271  ordtrest2  17273  lmcnp  17373  tgcmp  17469  uncmp  17471  hauscmplem  17474  1stcfb  17513  2ndcdisj  17524  kgencmp  17582  xkouni  17636  prdstopn  17665  txtube  17677  txcmplem2  17679  xkoptsub  17691  xkopt  17692  xkococnlem  17696  qtoprest  17754  imastopn  17757  kqdisj  17769  reghmph  17830  nrmhmph  17831  fbssfi  17874  trfilss  17926  trfg  17928  elfm3  17987  alexsubALTlem3  18085  alexsubALT  18087  cnextf  18102  cnextcn  18103  clsnsg  18144  tgpconcompeqg  18146  divstgphaus  18157  trust  18264  ustuqtop3  18278  neipcfilu  18331  metequiv2  18545  prdsxmslem2  18564  metustfbasOLD  18600  metustfbas  18601  icccmplem1  18858  metdstri  18886  pi1addf  19077  pi1addval  19078  caubl  19265  caublcls  19266  relcmpcmet  19274  minveclem4  19338  hlhil  19349  ovolficcss  19371  uniioombllem3a  19481  uniioombllem3  19482  dyadss  19491  opnmbllem  19498  i1fima2  19574  limcfval  19764  dvfval  19789  dvnres  19822  dvivth  19899  lhop  19905  evlseu  19942  taylf  20282  xrlimcnp  20812  jensen  20832  ppisval  20891  chtlepsi  20995  chpub  21009  chssoc  23003  mdsl0  23818  mdexchi  23843  atcvat3i  23904  dmdbr5ati  23930  funimass4f  24049  xrofsup  24131  cnvordtrestixx  24316  pnfneige0  24341  sigagenss  24537  imambfm  24617  dya2iocress  24629  dya2icoseg  24632  dya2iocucvr  24639  ballotlemro  24785  cvmlift3lem6  25016  relexpfld  25142  rtrclreclem.min  25152  trpredmintr  25514  nobndlem8  25659  liness  26084  opnmbllem0  26254  mblfinlem2  26256  neibastop2lem  26403  isbndx  26505  isbnd2  26506  ssbnd  26511  heiborlem3  26536  igenmin  26688  elrfi  26762  isnacs3  26778  mzpf  26807  mzpindd  26817  diophrw  26831  eldiophss  26847  rmxyelqirr  26987  pw2f1ocnv  27122  aomclem6  27148  frlmsplit2  27234  f1lindf  27283  hbt  27325  rgspnmin  27367  f1omvdco2  27382  pmtrfrn  27391  symgsssg  27399  symggen  27402  psgnunilem1  27407  bnj1097  29424  bnj1452  29495  lsatlss  29868  lsmsat  29880  lsatfixedN  29881  lssats  29884  lpssat  29885  lssatle  29887  lssat  29888  lsatcvat3  29924  paddssat  30685  paddasslem17  30707  pmodlem2  30718  hlmod1i  30727  pl42lem4N  30853  diassdvaN  31932  dia2dimlem10  31945  cdlemn4a  32071  cdlemn5pre  32072  dihord5apre  32134  lclkrlem2e  32383  lclkrlem2p  32394  lclkrlem2v  32400  lclkrslem2  32410  lclkrs  32411  lcfrlem25  32439  lcfrlem35  32449  mapdval2N  32502  mapdpglem8  32551  mapdpglem13  32556  baerlem3lem2  32582  mapdindp2  32593  hdmap11lem2  32717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator