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

Theorem eqsstrd 3342
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 3335 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 224 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3280
This theorem is referenced by:  eqsstr3d  3343  syl6eqss  3358  tfisi  4797  suppssof1  6305  riotassuni  6547  onfununi  6562  oawordeulem  6756  oeeui  6804  nnawordex  6839  oaabslem  6845  oaabs2  6847  omabslem  6848  omabs  6849  pw2f1olem  7171  fodomr  7217  fival  7375  dffi3  7394  ordtypelem7  7449  ordtypelem8  7450  wemapso2  7477  cantnflt2  7584  mapfien  7609  tcss  7639  tcel  7640  r1val1  7668  rankuni2b  7735  tcrank  7764  cardonle  7800  harval2  7840  carduniima  7933  ackbij2  8079  cfub  8085  cflecard  8089  cfflb  8095  isf32lem8  8196  itunitc1  8256  ttukeylem7  8351  fpwwe2lem9  8469  wuncss  8576  wuncval2  8578  grur1a  8650  limsupgre  12230  isercolllem3  12415  4sqlem19  13286  vdwlem1  13304  vdwlem12  13315  ramub1lem1  13349  ressress  13481  imasaddfnlem  13708  imasaddflem  13710  imasvscafn  13717  imasvscaf  13719  imasless  13720  isohom  13952  ressffth  14090  acsfiindd  14558  acsmap2d  14560  dirref  14635  sylow2alem2  15207  lsmssv  15232  lsmidm  15251  gsumzres  15472  dprdlub  15539  dprdf1  15546  dprdsn  15549  dprdcntz2  15551  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  ablfac1eu  15586  drnglpir  16279  issubassa2  16358  evlslem4  16519  znleval  16790  lpsscls  17160  tgrest  17177  resttopon  17179  rest0  17187  restfpw  17197  ordtrest  17220  ordtrest2  17222  lmcnp  17322  tgcmp  17418  uncmp  17420  hauscmplem  17423  1stcfb  17461  2ndcdisj  17472  kgencmp  17530  xkouni  17584  prdstopn  17613  txtube  17625  txcmplem2  17627  xkoptsub  17639  xkopt  17640  xkococnlem  17644  qtoprest  17702  imastopn  17705  kqdisj  17717  reghmph  17778  nrmhmph  17779  fbssfi  17822  trfilss  17874  trfg  17876  elfm3  17935  alexsubALTlem3  18033  alexsubALT  18035  cnextf  18050  cnextcn  18051  clsnsg  18092  tgpconcompeqg  18094  divstgphaus  18105  trust  18212  ustuqtop3  18226  neipcfilu  18279  metequiv2  18493  prdsxmslem2  18512  metustfbasOLD  18548  metustfbas  18549  icccmplem1  18806  metdstri  18834  pi1addf  19025  pi1addval  19026  caubl  19213  caublcls  19214  relcmpcmet  19222  minveclem4  19286  hlhil  19297  ovolficcss  19319  uniioombllem3a  19429  uniioombllem3  19430  dyadss  19439  opnmbllem  19446  i1fima2  19524  limcfval  19712  dvfval  19737  dvnres  19770  dvivth  19847  lhop  19853  evlseu  19890  taylf  20230  xrlimcnp  20760  jensen  20780  ppisval  20839  chtlepsi  20943  chpub  20957  chssoc  22951  mdsl0  23766  mdexchi  23791  atcvat3i  23852  dmdbr5ati  23878  funimass4f  23997  xrofsup  24079  cnvordtrestixx  24264  pnfneige0  24289  sigagenss  24485  imambfm  24565  dya2iocress  24577  dya2icoseg  24580  dya2iocucvr  24587  ballotlemro  24733  cvmlift3lem6  24964  relexpfld  25090  rtrclreclem.min  25100  trpredmintr  25448  nobndlem8  25567  liness  25983  mblfinlem  26143  neibastop2lem  26279  isbndx  26381  isbnd2  26382  ssbnd  26387  heiborlem3  26412  igenmin  26564  elrfi  26638  isnacs3  26654  mzpf  26683  mzpindd  26693  diophrw  26707  eldiophss  26723  rmxyelqirr  26863  pw2f1ocnv  26998  aomclem6  27024  frlmsplit2  27111  f1lindf  27160  hbt  27202  rgspnmin  27244  f1omvdco2  27259  pmtrfrn  27268  symgsssg  27276  symggen  27279  psgnunilem1  27284  bnj1097  29056  bnj1452  29127  lsatlss  29479  lsmsat  29491  lsatfixedN  29492  lssats  29495  lpssat  29496  lssatle  29498  lssat  29499  lsatcvat3  29535  paddssat  30296  paddasslem17  30318  pmodlem2  30329  hlmod1i  30338  pl42lem4N  30464  diassdvaN  31543  dia2dimlem10  31556  cdlemn4a  31682  cdlemn5pre  31683  dihord5apre  31745  lclkrlem2e  31994  lclkrlem2p  32005  lclkrlem2v  32011  lclkrslem2  32021  lclkrs  32022  lcfrlem25  32050  lcfrlem35  32060  mapdval2N  32113  mapdpglem8  32162  mapdpglem13  32167  baerlem3lem2  32193  mapdindp2  32204  hdmap11lem2  32328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator