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

Theorem eqsstrd 3434
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 3427 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 235 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3379  df-ss 3386
This theorem is referenced by:  eqsstr3d  3435  syl6eqss  3450  fpr2g  6077  tfisi  6636  suppssof1  6896  suppss2  6897  onfununi  7008  oawordeulem  7203  oeeui  7251  nnawordex  7286  oaabslem  7292  oaabs2  7294  omabslem  7295  omabs  7296  pw2f1olem  7622  fodomr  7669  fival  7872  dffi3  7891  ordtypelem7  7985  ordtypelem8  7986  wemapso2lem  8013  cantnflt2  8123  cantnflem1  8139  tcss  8173  tcel  8174  r1val1  8202  rankuni2b  8269  tcrank  8300  cardonle  8336  harval2  8376  carduniima  8471  ackbij2  8617  cfub  8623  cflecard  8627  cfflb  8633  isf32lem8  8734  itunitc1  8794  ttukeylem7  8889  fpwwe2lem9  9007  wuncss  9114  wuncval2  9116  grur1a  9188  trclfvub  13008  cotrtrclfv  13013  relexpfld  13049  rtrclreclem4  13061  limsupgre  13478  limsupgreOLD  13479  isercolllem3  13666  4sqlem19  14849  vdwlem1  14867  vdwlem12  14878  ramub1lem1  14920  ressress  15123  imasaddfnlem  15370  imasaddflem  15372  imasvscafn  15379  imasvscaf  15381  imasless  15382  isohom  15617  ressffth  15779  acsfiindd  16359  acsmap2d  16361  dirref  16417  mrcmndind  16549  f1omvdco2  17025  pmtrfrn  17035  symgsssg  17044  symggen  17047  psgnunilem1  17070  sylow2alem2  17206  lsmssv  17231  lsmidm  17250  gsumzres  17479  dprdlub  17595  dprdf1  17602  dprdsn  17605  dprdcntz2  17607  dprd2dlem1  17610  dprd2da  17611  dmdprdsplit2lem  17614  ablfac1eu  17642  drnglpir  18413  issubassa2  18505  evlslem4  18667  evlseu  18675  znleval  19060  evpmss  19089  frlmsplit2  19266  f1lindf  19315  lpsscls  20092  tgrest  20110  resttopon  20112  rest0  20120  restfpw  20130  ordtrest  20153  ordtrest2  20155  lmcnp  20255  tgcmp  20351  uncmp  20353  hauscmplem  20356  1stcfb  20395  2ndcdisj  20406  dissnref  20478  kgencmp  20495  xkouni  20549  prdstopn  20578  txtube  20590  txcmplem2  20592  xkoptsub  20604  xkopt  20605  xkococnlem  20609  qtoprest  20667  imastopn  20670  kqdisj  20682  reghmph  20743  nrmhmph  20744  fbssfi  20787  trfilss  20839  trfg  20841  elfm3  20900  alexsubALTlem3  20999  alexsubALT  21001  cnextf  21016  cnextcn  21017  clsnsg  21059  tgpconcompeqg  21061  qustgphaus  21072  trust  21179  ustuqtop3  21193  neipcfilu  21246  metequiv2  21460  prdsxmslem2  21479  metustfbas  21507  icccmplem1  21775  metdstri  21803  metdstriOLD  21818  pi1addf  22013  pi1addval  22014  caubl  22212  caublcls  22213  relcmpcmet  22221  minveclem4  22309  minveclem4OLD  22321  hlhil  22332  ovolficcss  22357  uniioombllem3a  22477  uniioombllem3  22478  dyadss  22487  opnmbllem  22494  i1fima2  22572  limcfval  22762  dvfval  22787  dvnres  22820  dvivth  22897  lhop  22903  taylf  23251  xrlimcnp  23829  jensen  23849  ppisval  23965  chtlepsi  24069  chpub  24083  iscgrglt  24494  edgss  25014  chssoc  27084  mdsl0  27898  mdexchi  27923  atcvat3i  27984  dmdbr5ati  28010  funimass4f  28173  xrofsup  28296  locfinreflem  28612  cmpcref  28622  cnvordtrestixx  28664  ordtrestNEW  28672  ordtrest2NEW  28674  pnfneige0  28702  sigagenss  28916  imambfm  29029  dya2iocress  29041  dya2icoseg  29044  dya2iocucvr  29051  ballotlemro  29300  ballotlemroOLD  29338  bnj1097  29735  bnj1452  29806  cvmlift3lem6  29992  msubrn  30112  mclsssv  30147  mclsind  30153  trpredmintr  30416  nobndlem8  30530  liness  30854  neibastop2lem  30958  opnmbllem0  31877  mblfinlem2  31879  isbndx  32015  isbnd2  32016  ssbnd  32021  heiborlem3  32046  igenmin  32198  lsatlss  32468  lsmsat  32480  lsatfixedN  32481  lssats  32484  lpssat  32485  lssatle  32487  lssat  32488  lsatcvat3  32524  paddssat  33285  paddasslem17  33307  pmodlem2  33318  hlmod1i  33327  pl42lem4N  33453  diassdvaN  34534  dia2dimlem10  34547  cdlemn4a  34673  cdlemn5pre  34674  dihord5apre  34736  lclkrlem2e  34985  lclkrlem2p  34996  lclkrlem2v  35002  lclkrslem2  35012  lclkrs  35013  lcfrlem25  35041  lcfrlem35  35051  mapdval2N  35104  mapdpglem8  35153  mapdpglem13  35158  baerlem3lem2  35184  mapdindp2  35195  hdmap11lem2  35319  elrfi  35442  isnacs3  35458  mzpf  35484  mzpindd  35494  diophrw  35507  eldiophss  35523  rmxyelqirr  35665  pw2f1ocnv  35799  aomclem6  35824  hbt  35896  rgspnmin  35944  cnvssb  36099  trclubgNEW  36132  dfrcl2  36173  fvmptiunrelexplb0da  36184  relexp0a  36215  cotrcltrcl  36224  trclimalb2  36225  cotrclrcl  36241  fnresdmss  37328  mptelpm  37338  mptss  37353  founiiun0  37363  ssnnf1octb  37368  uzfissfz  37440  iuneqfzuzlem  37448  icccncfext  37642  dvnprodlem1  37698  dvnprodlem2  37699  dvnprodlem3  37700  fourierdlem41  37888  fourierdlem70  37917  fourierdlem71  37918  fourierdlem80  37927  fourierdlem113  37960  iundjiun  38143  meadjiunlem  38148  meaiunlelem  38151  omeunle  38182  carageniuncllem2  38188  caratheodorylem1  38192  caratheodorylem2  38193  hoissre  38207  ovnsubaddlem1  38233  hoidmvlelem3  38260  ovnhoilem1  38264  ovnhoilem2  38265  ovnhoi  38266  uhgredg  38980  umgredgss  38981  edgass  39000  linc1  39805
  Copyright terms: Public domain W3C validator