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

Theorem eqsstrd 3378
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 3371 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 232 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  eqsstr3d  3379  syl6eqss  3394  suppssof1OLD  6328  tfisi  6458  suppssof1  6711  suppss2  6712  onfununi  6788  oawordeulem  6981  oeeui  7029  nnawordex  7064  oaabslem  7070  oaabs2  7072  omabslem  7073  omabs  7074  pw2f1olem  7403  fodomr  7450  fival  7650  dffi3  7669  ordtypelem7  7726  ordtypelem8  7727  wemapso2OLD  7754  wemapso2lem  7755  cantnflt2  7869  cantnflem1  7885  cantnflt2OLD  7899  mapfienOLD  7915  tcss  7952  tcel  7953  r1val1  7981  rankuni2b  8048  tcrank  8079  cardonle  8115  harval2  8155  carduniima  8254  ackbij2  8400  cfub  8406  cflecard  8410  cfflb  8416  isf32lem8  8517  itunitc1  8577  ttukeylem7  8672  fpwwe2lem9  8792  wuncss  8899  wuncval2  8901  grur1a  8973  limsupgre  12942  isercolllem3  13127  4sqlem19  14006  vdwlem1  14024  vdwlem12  14035  ramub1lem1  14069  ressress  14217  imasaddfnlem  14448  imasaddflem  14450  imasvscafn  14457  imasvscaf  14459  imasless  14460  isohom  14692  ressffth  14830  acsfiindd  15329  acsmap2d  15331  dirref  15387  mrcmndind  15475  f1omvdco2  15933  pmtrfrn  15943  symgsssg  15952  symggen  15955  psgnunilem1  15978  sylow2alem2  16096  lsmssv  16121  lsmidm  16140  gsumzres  16367  gsumzresOLD  16371  dprdlub  16496  dprdf1  16503  dprdsn  16506  dprdcntz2  16509  dprd2dlem1  16513  dprd2da  16514  dmdprdsplit2lem  16517  ablfac1eu  16547  drnglpir  17256  issubassa2  17336  evlslem4OLD  17517  evlslem4  17518  znleval  17828  evpmss  17857  frlmsplit2  18038  f1lindf  18092  lpsscls  18586  tgrest  18604  resttopon  18606  rest0  18614  restfpw  18624  ordtrest  18647  ordtrest2  18649  lmcnp  18749  tgcmp  18845  uncmp  18847  hauscmplem  18850  1stcfb  18890  2ndcdisj  18901  kgencmp  18959  xkouni  19013  prdstopn  19042  txtube  19054  txcmplem2  19056  xkoptsub  19068  xkopt  19069  xkococnlem  19073  qtoprest  19131  imastopn  19134  kqdisj  19146  reghmph  19207  nrmhmph  19208  fbssfi  19251  trfilss  19303  trfg  19305  elfm3  19364  alexsubALTlem3  19462  alexsubALT  19464  cnextf  19479  cnextcn  19480  clsnsg  19521  tgpconcompeqg  19523  divstgphaus  19534  trust  19645  ustuqtop3  19659  neipcfilu  19712  metequiv2  19926  prdsxmslem2  19945  metustfbasOLD  19981  metustfbas  19982  icccmplem1  20240  metdstri  20268  pi1addf  20460  pi1addval  20461  caubl  20659  caublcls  20660  relcmpcmet  20668  minveclem4  20760  hlhil  20771  ovolficcss  20794  uniioombllem3a  20905  uniioombllem3  20906  dyadss  20915  opnmbllem  20922  i1fima2  20998  limcfval  21188  dvfval  21213  dvnres  21246  dvivth  21323  lhop  21329  evlseu  21367  taylf  21710  xrlimcnp  22246  jensen  22266  ppisval  22325  chtlepsi  22429  chpub  22443  chssoc  24721  mdsl0  25536  mdexchi  25561  atcvat3i  25622  dmdbr5ati  25648  funimass4f  25774  xrofsup  25877  cnvordtrestixx  26196  ordtrestNEW  26204  ordtrest2NEW  26206  pnfneige0  26234  sigagenss  26445  imambfm  26530  dya2iocress  26542  dya2icoseg  26545  dya2iocucvr  26552  ballotlemro  26752  cvmlift3lem6  27060  relexpfld  27185  rtrclreclem.min  27195  trpredmintr  27541  nobndlem8  27686  liness  28022  opnmbllem0  28268  mblfinlem2  28270  neibastop2lem  28422  isbndx  28522  isbnd2  28523  ssbnd  28528  heiborlem3  28553  igenmin  28705  elrfi  28872  isnacs3  28888  mzpf  28914  mzpindd  28924  diophrw  28939  eldiophss  28955  rmxyelqirr  29093  pw2f1ocnv  29228  aomclem6  29254  hbt  29328  rgspnmin  29370  linc1  30665  bnj1097  31671  bnj1452  31742  lsatlss  32211  lsmsat  32223  lsatfixedN  32224  lssats  32227  lpssat  32228  lssatle  32230  lssat  32231  lsatcvat3  32267  paddssat  33028  paddasslem17  33050  pmodlem2  33061  hlmod1i  33070  pl42lem4N  33196  diassdvaN  34275  dia2dimlem10  34288  cdlemn4a  34414  cdlemn5pre  34415  dihord5apre  34477  lclkrlem2e  34726  lclkrlem2p  34737  lclkrlem2v  34743  lclkrslem2  34753  lclkrs  34754  lcfrlem25  34782  lcfrlem35  34792  mapdval2N  34845  mapdpglem8  34894  mapdpglem13  34899  baerlem3lem2  34925  mapdindp2  34936  hdmap11lem2  35060
  Copyright terms: Public domain W3C validator