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

Theorem eqsstrd 3395
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 3388 . 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 1369    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347
This theorem is referenced by:  eqsstr3d  3396  syl6eqss  3411  suppssof1OLD  6344  tfisi  6474  suppssof1  6727  suppss2  6728  onfununi  6807  oawordeulem  6998  oeeui  7046  nnawordex  7081  oaabslem  7087  oaabs2  7089  omabslem  7090  omabs  7091  pw2f1olem  7420  fodomr  7467  fival  7667  dffi3  7686  ordtypelem7  7743  ordtypelem8  7744  wemapso2OLD  7771  wemapso2lem  7772  cantnflt2  7886  cantnflem1  7902  cantnflt2OLD  7916  mapfienOLD  7932  tcss  7969  tcel  7970  r1val1  7998  rankuni2b  8065  tcrank  8096  cardonle  8132  harval2  8172  carduniima  8271  ackbij2  8417  cfub  8423  cflecard  8427  cfflb  8433  isf32lem8  8534  itunitc1  8594  ttukeylem7  8689  fpwwe2lem9  8810  wuncss  8917  wuncval2  8919  grur1a  8991  limsupgre  12964  isercolllem3  13149  4sqlem19  14029  vdwlem1  14047  vdwlem12  14058  ramub1lem1  14092  ressress  14240  imasaddfnlem  14471  imasaddflem  14473  imasvscafn  14480  imasvscaf  14482  imasless  14483  isohom  14715  ressffth  14853  acsfiindd  15352  acsmap2d  15354  dirref  15410  mrcmndind  15499  f1omvdco2  15959  pmtrfrn  15969  symgsssg  15978  symggen  15981  psgnunilem1  16004  sylow2alem2  16122  lsmssv  16147  lsmidm  16166  gsumzres  16393  gsumzresOLD  16397  dprdlub  16528  dprdf1  16535  dprdsn  16538  dprdcntz2  16541  dprd2dlem1  16545  dprd2da  16546  dmdprdsplit2lem  16549  ablfac1eu  16579  drnglpir  17340  issubassa2  17420  evlslem4OLD  17595  evlslem4  17596  evlseu  17607  znleval  17992  evpmss  18021  frlmsplit2  18202  f1lindf  18256  lpsscls  18750  tgrest  18768  resttopon  18770  rest0  18778  restfpw  18788  ordtrest  18811  ordtrest2  18813  lmcnp  18913  tgcmp  19009  uncmp  19011  hauscmplem  19014  1stcfb  19054  2ndcdisj  19065  kgencmp  19123  xkouni  19177  prdstopn  19206  txtube  19218  txcmplem2  19220  xkoptsub  19232  xkopt  19233  xkococnlem  19237  qtoprest  19295  imastopn  19298  kqdisj  19310  reghmph  19371  nrmhmph  19372  fbssfi  19415  trfilss  19467  trfg  19469  elfm3  19528  alexsubALTlem3  19626  alexsubALT  19628  cnextf  19643  cnextcn  19644  clsnsg  19685  tgpconcompeqg  19687  divstgphaus  19698  trust  19809  ustuqtop3  19823  neipcfilu  19876  metequiv2  20090  prdsxmslem2  20109  metustfbasOLD  20145  metustfbas  20146  icccmplem1  20404  metdstri  20432  pi1addf  20624  pi1addval  20625  caubl  20823  caublcls  20824  relcmpcmet  20832  minveclem4  20924  hlhil  20935  ovolficcss  20958  uniioombllem3a  21069  uniioombllem3  21070  dyadss  21079  opnmbllem  21086  i1fima2  21162  limcfval  21352  dvfval  21377  dvnres  21410  dvivth  21487  lhop  21493  taylf  21831  xrlimcnp  22367  jensen  22387  ppisval  22446  chtlepsi  22550  chpub  22564  chssoc  24904  mdsl0  25719  mdexchi  25744  atcvat3i  25805  dmdbr5ati  25831  funimass4f  25956  xrofsup  26060  cnvordtrestixx  26348  ordtrestNEW  26356  ordtrest2NEW  26358  pnfneige0  26386  sigagenss  26597  imambfm  26682  dya2iocress  26694  dya2icoseg  26697  dya2iocucvr  26704  ballotlemro  26910  cvmlift3lem6  27218  relexpfld  27344  rtrclreclem.min  27354  trpredmintr  27700  nobndlem8  27845  liness  28181  opnmbllem0  28432  mblfinlem2  28434  neibastop2lem  28586  isbndx  28686  isbnd2  28687  ssbnd  28692  heiborlem3  28717  igenmin  28869  elrfi  29035  isnacs3  29051  mzpf  29077  mzpindd  29087  diophrw  29102  eldiophss  29118  rmxyelqirr  29256  pw2f1ocnv  29391  aomclem6  29417  hbt  29491  rgspnmin  29533  pmatcollpw1lem4  30907  linc1  30964  bnj1097  31977  bnj1452  32048  lsatlss  32646  lsmsat  32658  lsatfixedN  32659  lssats  32662  lpssat  32663  lssatle  32665  lssat  32666  lsatcvat3  32702  paddssat  33463  paddasslem17  33485  pmodlem2  33496  hlmod1i  33505  pl42lem4N  33631  diassdvaN  34710  dia2dimlem10  34723  cdlemn4a  34849  cdlemn5pre  34850  dihord5apre  34912  lclkrlem2e  35161  lclkrlem2p  35172  lclkrlem2v  35178  lclkrslem2  35188  lclkrs  35189  lcfrlem25  35217  lcfrlem35  35227  mapdval2N  35280  mapdpglem8  35329  mapdpglem13  35334  baerlem3lem2  35360  mapdindp2  35371  hdmap11lem2  35495
  Copyright terms: Public domain W3C validator