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

Theorem sseqtr4d 3437
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtr4d.1  |-  ( ph  ->  A  C_  B )
sseqtr4d.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
sseqtr4d  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtr4d
StepHypRef Expression
1 sseqtr4d.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtr4d.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2458 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3436 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1448    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386
This theorem is referenced by:  syl5sseqr  3449  fnfvima  6129  wfrlem17  7039  oaordi  7234  omordi  7254  omlimcl  7266  oen0  7274  domunsncan  7659  f1opwfi  7865  cantnfle  8163  cantnflt  8164  cantnflem1d  8180  r1pwss  8242  rankxplim3  8339  acndom2  8472  fodomfi2  8478  cflm  8667  cflim2  8680  isf34lem5  8795  isf34lem7  8796  isf34lem6  8797  axdc2lem  8865  ttukeylem5  8930  wunex2  9150  ccatass  12730  swrdval2  12775  swrdccatin12  12846  splfv2a  12862  revccat  12870  rtrclreclem1  13132  rtrclreclem2  13133  sumrblem  13788  prodrblem  13994  dfphi2  14733  vdwlem1  14942  imasaddfnlem  15445  imasaddvallem  15446  imasvscafn  15454  imasvscaval  15455  mreexexlem4d  15564  mreexfidimd  15567  sscpwex  15731  acsmap2d  16436  gsumress  16530  subsubm  16615  frmdsssubm  16656  frmdss2  16658  subsubg  16851  cntzmhm2  17004  cntzcmnf  17494  ablcntzd  17506  gsumzsubmcl  17562  gsumconst  17578  gsumzmhm  17581  gsumzoppg  17588  subgdmdprd  17678  dprdcntz2  17682  dprd2da  17686  dmdprdsplit2lem  17689  ablfac1eu  17717  pgpfaclem1  17725  pgpfaclem2  17726  issubdrg  18044  subsubrg  18045  lmhmlsp  18283  lspsntri  18331  lspindpi  18366  lidldvgen  18490  opsrtoslem2  18719  gsumfsum  19045  mrccss  19268  frlmsslsp  19365  scmatsgrp1  19558  toponss  19955  ssntr  20084  elcls3  20110  toponmre  20120  neiptoptop  20158  neiptopnei  20159  neitr  20207  ordtbas  20219  ordtopn1  20221  ordtopn2  20222  iscnp3  20271  tgcn  20279  tgcnp  20280  ssidcn  20282  cnclsi  20299  cncls  20301  cncnp  20307  lmcld  20330  tgcmp  20427  cnconn  20448  conima  20451  clscon  20456  concompcld  20460  1stccnp  20488  kgentopon  20564  llycmpkgen2  20576  1stckgen  20580  kgencn2  20583  ptopn  20609  txcls  20630  ptpjcn  20637  ptclsg  20641  xkoccn  20645  txcnp  20646  ptcnplem  20647  txcmplem2  20668  xkoptsub  20680  xkopt  20681  xkoco2cn  20684  xkococnlem  20685  xkoinjcn  20713  imasnopn  20716  imasncld  20717  imasncls  20718  qtopkgen  20736  basqtop  20737  tgqtop  20738  qtoprest  20743  kqsat  20757  kqcldsat  20759  kqnrmlem1  20769  kqnrmlem2  20770  hmeontr  20795  reghmph  20819  nrmhmph  20820  fmfnfmlem4  20983  fmfnfm  20984  flimopn  21001  flimclslem  21010  flfnei  21017  lmflf  21031  txflf  21032  fclsopn  21040  fclsfnflim  21053  alexsublem  21070  ptcmplem3  21080  cnextcn  21093  symgtgp  21127  submtmd  21130  subgtgp  21131  clssubg  21134  clsnsg  21135  tgpconcompeqg  21137  snclseqg  21141  tsmscls  21163  trust  21255  restutop  21263  restutopopn  21264  utop3cls  21277  utopreg  21278  trcfilu  21320  blssec  21461  prdsbl  21517  blssopn  21521  metcnp  21567  cfilucfil  21585  psmetutop  21593  iccntr  21850  icccmplem2  21852  reconnlem1  21855  metnrmlem1a  21886  metnrmlem1  21887  metnrmlem2  21888  metnrmlem3  21889  metnrmlem1aOLD  21901  metnrmlem1OLD  21902  metnrmlem2OLD  21903  metnrmlem3OLD  21904  cnheibor  21994  lebnumlem1  22000  lebnumlem3  22002  lebnumlem1OLD  22003  lebnumlem3OLD  22005  lebnumii  22008  clsocv  22232  iscfil2  22247  iscmet3  22274  cmetss  22295  relcmpcmet  22297  bcthlem5  22307  itg1addlem5  22670  perfdvf  22870  dvres3  22880  dvres3a  22881  dvcmul  22910  dvcmulf  22911  dvlip2  22959  lhop1lem  22977  dvcnvrelem1  22981  dvcnvrelem2  22982  dvcnvre  22983  dvcvx  22984  plyco0  23158  plyaddlem1  23179  plymullem1  23180  aalioulem3  23302  ulmdvlem1  23367  axcontlem10  25015  eengtrkg  25027  eupares  25715  ghsubgolemOLD  26110  hsupunss  27008  pjpjpre  27084  ssmd2  27977  superpos  28019  atexch  28046  curry2ima  28297  madjusmdetlem2  28661  ordtconlem1  28737  measiuns  29046  imambfm  29090  cnmbfm  29091  dya2iocnrect  29109  omsfval  29124  omsfvalOLD  29128  omssubaddlem  29133  omssubadd  29134  omssubaddlemOLD  29137  omssubaddOLD  29138  totprobd  29265  fzssfzo  29428  signstfvn  29464  bnj999  29774  bnj1408  29851  bnj1442  29864  bnj1450  29865  bnj1501  29882  cvmsss2  30003  cvmliftmolem1  30010  cvmliftlem3  30016  cvmlift2lem9  30040  cvmlift2lem11  30042  cvmlift3lem6  30053  cvmlift3lem7  30054  ssmclslem  30209  mclsax  30213  mclsppslem  30227  mclspps  30228  dfrdg2  30448  trpredtr  30477  neiin  30994  neibastop2  31023  filnetlem4  31043  poimirlem11  31953  poimirlem12  31954  itg2addnclem2  31996  cnres2  32097  sstotbnd2  32108  sstotbnd  32109  prdstotbnd  32128  heibor1lem  32143  igenval2  32301  lshpnelb  32552  lcvexchlem4  32605  lsatexch  32611  l1cvat  32623  lkrscss  32666  lkrss  32736  lkreqN  32738  paddunN  33494  osumcllem2N  33524  pmapojoinN  33535  pl42lem2N  33547  dibglbN  34736  diblss  34740  dicvaddcl  34760  dicvscacl  34761  diclss  34763  cdlemn5pre  34770  dihord5apre  34832  dihglblem3N  34865  dihglb2  34912  dochsat  34953  dochshpncl  34954  djhspss  34976  dihsumssj  34978  mapdlsm  35234  hdmaprnlem3eN  35431  hdmaplkr  35486  fnwe2lem2  35911  lnmlsslnm  35941  lmhmfgima  35944  hbtlem6  35990  trrelsuperreldg  36262  iunrelexpuztr  36313  funfvima2d  36614  dvsconst  36680  dvsinax  37825  dvbdfbdioolem1  37842  itgsinexplem1  37872  itgperiod  37900  stoweidlem39  37957  dirkeritg  38021  fourierdlem48  38075  fourierdlem49  38076  fourierdlem70  38097  fourierdlem71  38098  fourierdlem81  38108  issalgend  38254  pfxccatin12  39059  nbupgruvtxres  39582  11wlkdlem4  39907  subsubmgm  40122  rmsuppss  40480
  Copyright terms: Public domain W3C validator