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

Theorem eqsstrd 3538
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 3531 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  eqsstr3d  3539  syl6eqss  3554  suppssof1OLD  6541  tfisi  6671  suppssof1  6930  suppss2  6931  onfununi  7009  oawordeulem  7200  oeeui  7248  nnawordex  7283  oaabslem  7289  oaabs2  7291  omabslem  7292  omabs  7293  pw2f1olem  7618  fodomr  7665  fival  7868  dffi3  7887  ordtypelem7  7945  ordtypelem8  7946  wemapso2OLD  7973  wemapso2lem  7974  cantnflt2  8088  cantnflem1  8104  cantnflt2OLD  8118  mapfienOLD  8134  tcss  8171  tcel  8172  r1val1  8200  rankuni2b  8267  tcrank  8298  cardonle  8334  harval2  8374  carduniima  8473  ackbij2  8619  cfub  8625  cflecard  8629  cfflb  8635  isf32lem8  8736  itunitc1  8796  ttukeylem7  8891  fpwwe2lem9  9012  wuncss  9119  wuncval2  9121  grur1a  9193  limsupgre  13263  isercolllem3  13448  4sqlem19  14336  vdwlem1  14354  vdwlem12  14365  ramub1lem1  14399  ressress  14548  imasaddfnlem  14779  imasaddflem  14781  imasvscafn  14788  imasvscaf  14790  imasless  14791  isohom  15023  ressffth  15161  acsfiindd  15660  acsmap2d  15662  dirref  15718  mrcmndind  15807  f1omvdco2  16269  pmtrfrn  16279  symgsssg  16288  symggen  16291  psgnunilem1  16314  sylow2alem2  16434  lsmssv  16459  lsmidm  16478  gsumzres  16705  gsumzresOLD  16709  dprdlub  16863  dprdf1  16870  dprdsn  16873  dprdcntz2  16876  dprd2dlem1  16880  dprd2da  16881  dmdprdsplit2lem  16884  ablfac1eu  16914  drnglpir  17683  issubassa2  17765  evlslem4OLD  17944  evlslem4  17945  evlseu  17956  znleval  18360  evpmss  18389  frlmsplit2  18570  f1lindf  18624  lpsscls  19408  tgrest  19426  resttopon  19428  rest0  19436  restfpw  19446  ordtrest  19469  ordtrest2  19471  lmcnp  19571  tgcmp  19667  uncmp  19669  hauscmplem  19672  1stcfb  19712  2ndcdisj  19723  kgencmp  19781  xkouni  19835  prdstopn  19864  txtube  19876  txcmplem2  19878  xkoptsub  19890  xkopt  19891  xkococnlem  19895  qtoprest  19953  imastopn  19956  kqdisj  19968  reghmph  20029  nrmhmph  20030  fbssfi  20073  trfilss  20125  trfg  20127  elfm3  20186  alexsubALTlem3  20284  alexsubALT  20286  cnextf  20301  cnextcn  20302  clsnsg  20343  tgpconcompeqg  20345  divstgphaus  20356  trust  20467  ustuqtop3  20481  neipcfilu  20534  metequiv2  20748  prdsxmslem2  20767  metustfbasOLD  20803  metustfbas  20804  icccmplem1  21062  metdstri  21090  pi1addf  21282  pi1addval  21283  caubl  21481  caublcls  21482  relcmpcmet  21490  minveclem4  21582  hlhil  21593  ovolficcss  21616  uniioombllem3a  21728  uniioombllem3  21729  dyadss  21738  opnmbllem  21745  i1fima2  21821  limcfval  22011  dvfval  22036  dvnres  22069  dvivth  22146  lhop  22152  taylf  22490  xrlimcnp  23026  jensen  23046  ppisval  23105  chtlepsi  23209  chpub  23223  edgss  24028  chssoc  26090  mdsl0  26905  mdexchi  26930  atcvat3i  26991  dmdbr5ati  27017  funimass4f  27147  xrofsup  27250  cnvordtrestixx  27531  ordtrestNEW  27539  ordtrest2NEW  27541  pnfneige0  27569  sigagenss  27789  imambfm  27873  dya2iocress  27885  dya2icoseg  27888  dya2iocucvr  27895  ballotlemro  28101  cvmlift3lem6  28409  relexpfld  28535  rtrclreclem.min  28545  trpredmintr  28891  nobndlem8  29036  liness  29372  opnmbllem0  29627  mblfinlem2  29629  neibastop2lem  29781  isbndx  29881  isbnd2  29882  ssbnd  29887  heiborlem3  29912  igenmin  30064  elrfi  30230  isnacs3  30246  mzpf  30272  mzpindd  30282  diophrw  30296  eldiophss  30312  rmxyelqirr  30450  pw2f1ocnv  30583  aomclem6  30609  hbt  30683  rgspnmin  30725  islptre  31161  icccncfext  31226  ibliooicc  31289  fourierdlem41  31448  fourierdlem70  31477  fourierdlem71  31478  fourierdlem80  31487  fourierdlem113  31520  linc1  32099  bnj1097  33116  bnj1452  33187  lsatlss  33793  lsmsat  33805  lsatfixedN  33806  lssats  33809  lpssat  33810  lssatle  33812  lssat  33813  lsatcvat3  33849  paddssat  34610  paddasslem17  34632  pmodlem2  34643  hlmod1i  34652  pl42lem4N  34778  diassdvaN  35857  dia2dimlem10  35870  cdlemn4a  35996  cdlemn5pre  35997  dihord5apre  36059  lclkrlem2e  36308  lclkrlem2p  36319  lclkrlem2v  36325  lclkrslem2  36335  lclkrs  36336  lcfrlem25  36364  lcfrlem35  36374  mapdval2N  36427  mapdpglem8  36476  mapdpglem13  36481  baerlem3lem2  36507  mapdindp2  36518  hdmap11lem2  36642
  Copyright terms: Public domain W3C validator