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

Theorem sseqtr4d 3381
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 2438 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3380 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  syl5sseqr  3393  reusv6OLD  4491  fnfvima  5942  oaordi  6973  omordi  6993  omlimcl  7005  oen0  7013  domunsncan  7399  f1opwfi  7603  cantnfle  7867  cantnflt  7868  cantnflem1d  7884  cantnfleOLD  7897  cantnfltOLD  7898  cantnflem1dOLD  7907  r1pwss  7979  rankxplim3  8076  acndom2  8212  fodomfi2  8218  cflm  8407  cflim2  8420  isf34lem5  8535  isf34lem7  8536  isf34lem6  8537  axdc2lem  8605  ttukeylem5  8670  wunex2  8892  ccatass  12269  swrdval2  12299  swrdccatin12  12365  splfv2a  12381  revccat  12389  sumrblem  13171  dfphi2  13831  vdwlem1  14024  imasaddfnlem  14448  imasaddvallem  14449  imasvscafn  14457  imasvscaval  14458  mreexexlem4d  14567  mreexfidimd  14570  sscpwex  14710  acsmap2d  15331  subsubm  15466  gsumress  15486  frmdsssubm  15518  frmdss2  15520  subsubg  15683  cntzmhm2  15836  cntzcmnf  16306  ablcntzd  16318  gsumzsubmcl  16381  gsumzsubmclOLD  16382  gsumzmhm  16406  gsumzmhmOLD  16407  subgdmdprd  16504  dprdcntz2  16509  dprd2da  16514  dmdprdsplit2lem  16517  ablfac1eu  16547  pgpfaclem1  16555  pgpfaclem2  16556  issubdrg  16813  subsubrg  16814  lmhmlsp  17051  lspsntri  17099  lspindpi  17134  lidldvgen  17258  opsrtoslem2  17497  gsumfsum  17722  mrccss  17960  frlmsslsp  18064  frlmsslspOLD  18065  toponss  18375  ssntr  18503  elcls3  18528  toponmre  18538  neiptoptop  18576  neiptopnei  18577  neitr  18625  ordtbas  18637  ordtopn1  18639  ordtopn2  18640  iscnp3  18689  tgcn  18697  tgcnp  18698  ssidcn  18700  cnclsi  18717  cncls  18719  cncnp  18725  cnrest  18730  lmcld  18748  tgcmp  18845  cnconn  18867  conima  18870  clscon  18875  concompcld  18879  1stccnp  18907  kgentopon  18952  llycmpkgen2  18964  1stckgen  18968  kgencn2  18971  ptopn  18997  txcls  19018  ptpjcn  19025  ptclsg  19029  xkoccn  19033  txcnp  19034  ptcnplem  19035  txcmplem2  19056  xkoptsub  19068  xkopt  19069  xkoco2cn  19072  xkococnlem  19073  xkoinjcn  19101  imasnopn  19104  imasncld  19105  imasncls  19106  qtopkgen  19124  basqtop  19125  tgqtop  19126  qtoprest  19131  kqsat  19145  kqcldsat  19147  kqnrmlem1  19157  kqnrmlem2  19158  hmeontr  19183  reghmph  19207  nrmhmph  19208  fmfnfmlem4  19371  fmfnfm  19372  flimopn  19389  flimclslem  19398  flfnei  19405  lmflf  19419  txflf  19420  fclsopn  19428  fclsfnflim  19441  alexsublem  19457  ptcmplem3  19467  cnextcn  19480  symgtgp  19513  submtmd  19516  subgtgp  19517  clssubg  19520  clsnsg  19521  tgpconcompeqg  19523  snclseqg  19527  tsmscls  19549  trust  19645  restutop  19653  restutopopn  19654  utop3cls  19667  utopreg  19668  trcfilu  19710  blssec  19851  prdsbl  19907  blssopn  19911  metcnp  19957  cfilucfilOLD  19985  cfilucfil  19986  metutopOLD  19998  psmetutop  19999  iccntr  20239  icccmplem2  20241  reconnlem1  20244  metnrmlem1a  20275  metnrmlem1  20276  metnrmlem2  20277  metnrmlem3  20278  cnheibor  20368  lebnumlem1  20374  lebnumlem3  20376  lebnumii  20379  clsocv  20603  iscfil2  20618  iscmet3  20645  cmetss  20666  relcmpcmet  20668  bcthlem5  20680  itg1addlem5  21019  perfdvf  21219  dvres3  21229  dvres3a  21230  dvcmul  21259  dvcmulf  21260  dvlip2  21308  lhop1lem  21326  dvcnvrelem1  21330  dvcnvrelem2  21331  dvcnvre  21332  dvcvx  21333  plyco0  21544  plyaddlem1  21565  plymullem1  21566  aalioulem3  21684  ulmdvlem1  21749  axcontlem10  23041  eengtrkg  23053  eupares  23418  ghsubgolem  23679  hsupunss  24568  pjpjpre  24644  ssmd2  25538  superpos  25580  atexch  25607  curry2ima  25826  ordtconlem1  26207  measiuns  26484  imambfm  26530  cnmbfm  26531  dya2iocnrect  26549  sitgclg  26575  totprobd  26656  fzssfzo  26781  signstfvn  26817  cvmsss2  27010  cvmliftmolem1  27017  cvmliftlem3  27023  cvmlift2lem9  27047  cvmlift2lem11  27049  cvmlift3lem6  27060  cvmlift3lem7  27061  rtrclreclem.refl  27192  rtrclreclem.subset  27193  prodrblem  27288  dfrdg2  27455  trpredtr  27540  itg2addnclem2  28285  neiin  28368  neibastop2  28423  filnetlem4  28443  cnres2  28503  sstotbnd2  28514  sstotbnd  28515  prdstotbnd  28534  heibor1lem  28549  igenval2  28707  fnwe2lem2  29246  lnmlsslnm  29276  lmhmfgima  29279  hbtlem6  29327  dvsconst  29446  itgsinexplem1  29637  stoweidlem39  29677  rmsuppss  30611  bnj999  31649  bnj1408  31726  bnj1442  31739  bnj1450  31740  bnj1501  31757  lshpnelb  32199  lcvexchlem4  32252  lsatexch  32258  l1cvat  32270  lkrscss  32313  lkrss  32383  lkreqN  32385  paddunN  33141  osumcllem2N  33171  pmapojoinN  33182  pl42lem2N  33194  dibglbN  34381  diblss  34385  dicvaddcl  34405  dicvscacl  34406  diclss  34408  cdlemn5pre  34415  dihord5apre  34477  dihglblem3N  34510  dihglb2  34557  dochsat  34598  dochshpncl  34599  djhspss  34621  dihsumssj  34623  mapdlsm  34879  hdmaprnlem3eN  35076  hdmaplkr  35131
  Copyright terms: Public domain W3C validator