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

Theorem eqsstrd 3523
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 3516 . 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 1398    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  eqsstr3d  3524  syl6eqss  3539  suppssof1OLD  6532  tfisi  6666  suppssof1  6925  suppss2  6926  onfununi  7004  oawordeulem  7195  oeeui  7243  nnawordex  7278  oaabslem  7284  oaabs2  7286  omabslem  7287  omabs  7288  pw2f1olem  7614  fodomr  7661  fival  7864  dffi3  7883  ordtypelem7  7941  ordtypelem8  7942  wemapso2OLD  7969  wemapso2lem  7970  cantnflt2  8083  cantnflem1  8099  cantnflt2OLD  8113  mapfienOLD  8129  tcss  8166  tcel  8167  r1val1  8195  rankuni2b  8262  tcrank  8293  cardonle  8329  harval2  8369  carduniima  8468  ackbij2  8614  cfub  8620  cflecard  8624  cfflb  8630  isf32lem8  8731  itunitc1  8791  ttukeylem7  8886  fpwwe2lem9  9005  wuncss  9112  wuncval2  9114  grur1a  9186  trclfvub  12928  cotrtrclfv  12933  relexpfld  12967  rtrclreclem4  12979  limsupgre  13389  isercolllem3  13574  4sqlem19  14568  vdwlem1  14586  vdwlem12  14597  ramub1lem1  14631  ressress  14784  imasaddfnlem  15020  imasaddflem  15022  imasvscafn  15029  imasvscaf  15031  imasless  15032  isohom  15267  ressffth  15429  acsfiindd  16009  acsmap2d  16011  dirref  16067  mrcmndind  16199  f1omvdco2  16675  pmtrfrn  16685  symgsssg  16694  symggen  16697  psgnunilem1  16720  sylow2alem2  16840  lsmssv  16865  lsmidm  16884  gsumzres  17116  gsumzresOLD  17120  dprdlub  17271  dprdf1  17278  dprdsn  17281  dprdcntz2  17284  dprd2dlem1  17288  dprd2da  17289  dmdprdsplit2lem  17292  ablfac1eu  17322  drnglpir  18099  issubassa2  18192  evlslem4OLD  18371  evlslem4  18372  evlseu  18383  znleval  18769  evpmss  18798  frlmsplit2  18977  f1lindf  19027  lpsscls  19812  tgrest  19830  resttopon  19832  rest0  19840  restfpw  19850  ordtrest  19873  ordtrest2  19875  lmcnp  19975  tgcmp  20071  uncmp  20073  hauscmplem  20076  1stcfb  20115  2ndcdisj  20126  dissnref  20198  kgencmp  20215  xkouni  20269  prdstopn  20298  txtube  20310  txcmplem2  20312  xkoptsub  20324  xkopt  20325  xkococnlem  20329  qtoprest  20387  imastopn  20390  kqdisj  20402  reghmph  20463  nrmhmph  20464  fbssfi  20507  trfilss  20559  trfg  20561  elfm3  20620  alexsubALTlem3  20718  alexsubALT  20720  cnextf  20735  cnextcn  20736  clsnsg  20777  tgpconcompeqg  20779  qustgphaus  20790  trust  20901  ustuqtop3  20915  neipcfilu  20968  metequiv2  21182  prdsxmslem2  21201  metustfbasOLD  21237  metustfbas  21238  icccmplem1  21496  metdstri  21524  pi1addf  21716  pi1addval  21717  caubl  21915  caublcls  21916  relcmpcmet  21924  minveclem4  22016  hlhil  22027  ovolficcss  22050  uniioombllem3a  22162  uniioombllem3  22163  dyadss  22172  opnmbllem  22179  i1fima2  22255  limcfval  22445  dvfval  22470  dvnres  22503  dvivth  22580  lhop  22586  taylf  22925  xrlimcnp  23499  jensen  23519  ppisval  23578  chtlepsi  23682  chpub  23696  edgss  24557  chssoc  26615  mdsl0  27430  mdexchi  27455  atcvat3i  27516  dmdbr5ati  27542  funimass4f  27698  xrofsup  27819  locfinreflem  28081  cmpcref  28091  cnvordtrestixx  28133  ordtrestNEW  28141  ordtrest2NEW  28143  pnfneige0  28171  sigagenss  28382  imambfm  28473  dya2iocress  28485  dya2icoseg  28488  dya2iocucvr  28495  ballotlemro  28728  cvmlift3lem6  29036  msubrn  29156  mclsssv  29191  mclsind  29197  trpredmintr  29557  nobndlem8  29702  liness  30026  opnmbllem0  30293  mblfinlem2  30295  neibastop2lem  30421  isbndx  30521  isbnd2  30522  ssbnd  30527  heiborlem3  30552  igenmin  30704  elrfi  30869  isnacs3  30885  mzpf  30911  mzpindd  30921  diophrw  30934  eldiophss  30950  rmxyelqirr  31088  pw2f1ocnv  31221  aomclem6  31247  hbt  31323  rgspnmin  31364  fnresdmss  31686  mptelpm  31696  icccncfext  31932  dvnprodlem1  31985  dvnprodlem2  31986  dvnprodlem3  31987  fourierdlem41  32172  fourierdlem70  32201  fourierdlem71  32202  fourierdlem80  32211  fourierdlem113  32244  linc1  33299  bnj1097  34457  bnj1452  34528  lsatlss  35137  lsmsat  35149  lsatfixedN  35150  lssats  35153  lpssat  35154  lssatle  35156  lssat  35157  lsatcvat3  35193  paddssat  35954  paddasslem17  35976  pmodlem2  35987  hlmod1i  35996  pl42lem4N  36122  diassdvaN  37203  dia2dimlem10  37216  cdlemn4a  37342  cdlemn5pre  37343  dihord5apre  37405  lclkrlem2e  37654  lclkrlem2p  37665  lclkrlem2v  37671  lclkrslem2  37681  lclkrs  37682  lcfrlem25  37710  lcfrlem35  37720  mapdval2N  37773  mapdpglem8  37822  mapdpglem13  37827  baerlem3lem2  37853  mapdindp2  37864  hdmap11lem2  37988  dfrcl2  38214  relexp0a  38244  cotrclrcl  38253  cotrcltrcl  38254  trclimalb2  38260
  Copyright terms: Public domain W3C validator