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

Theorem sseqtrrd 3963
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrrd.1 (𝜑𝐴𝐵)
sseqtrrd.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
sseqtrrd (𝜑𝐴𝐶)

Proof of Theorem sseqtrrd
StepHypRef Expression
1 sseqtrrd.1 . 2 (𝜑𝐴𝐵)
2 sseqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2745 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 3962 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wss 3888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905
This theorem is referenced by:  sseqtrrid  3975  funfvima2d  7117  fnfvima  7118  frrlem8  8118  frrlem10  8120  fprresex  8135  wfrlem17OLD  8165  oaordi  8386  omordi  8406  omlimcl  8418  oen0  8426  domunsncan  8868  f1opwfi  9132  cantnfle  9438  cantnflt  9439  cantnflem1d  9455  ttrcltr  9483  r1pwss  9551  rankxplim3  9648  acndom2  9819  fodomfi2  9825  cflm  10015  cflim2  10028  isf34lem5  10143  isf34lem7  10144  isf34lem6  10145  axdc2lem  10213  ttukeylem5  10278  wunex2  10503  ssfzunsn  13311  ccatass  14302  swrdval2  14368  splfv2a  14478  revccat  14488  cshimadifsn  14551  cshimadifsn0  14552  rtrclreclem1  14777  rtrclreclem2  14779  sumrblem  15432  prodrblem  15648  dfphi2  16484  vdwlem1  16691  basprssdmsets  16934  imasaddfnlem  17248  imasaddvallem  17249  imasvscafn  17257  imasvscaval  17258  mreexexlem4d  17365  mreexfidimd  17368  sscpwex  17536  acsmap2d  18282  gsumress  18375  subsubm  18464  frmdsssubm  18509  frmdss2  18511  subsubg  18787  cntzmhm2  18955  cntzcmnf  19455  ablcntzd  19467  gsumzsubmcl  19528  gsumconst  19544  gsumzmhm  19547  subgdmdprd  19646  dprdcntz2  19650  dprd2da  19654  dmdprdsplit2lem  19657  ablfac1eu  19685  pgpfaclem1  19693  pgpfaclem2  19694  issubdrg  20058  subsubrg  20059  subdrgint  20080  lmhmlsp  20320  lspsntri  20368  lspindpi  20403  lidldvgen  20535  gsumfsum  20674  mrccss  20908  frlmsslsp  21012  opsrtoslem2  21272  scmatsgrp1  21680  toponss  22085  ssntr  22218  elcls3  22243  toponmre  22253  neiptoptop  22291  neiptopnei  22292  neitr  22340  ordtbas  22352  ordtopn1  22354  ordtopn2  22355  iscnp3  22404  tgcn  22412  tgcnp  22413  ssidcn  22415  cnclsi  22432  cncls  22434  cncnp  22440  lmcld  22463  tgcmp  22561  cnconn  22582  connima  22585  clsconn  22590  conncompcld  22594  1stccnp  22622  kgentopon  22698  llycmpkgen2  22710  1stckgen  22714  kgencn2  22717  ptopn  22743  txcls  22764  ptpjcn  22771  ptclsg  22775  xkoccn  22779  txcnp  22780  ptcnplem  22781  txcmplem2  22802  xkoptsub  22814  xkopt  22815  xkoco2cn  22818  xkococnlem  22819  xkoinjcn  22847  imasnopn  22850  imasncld  22851  imasncls  22852  qtopkgen  22870  basqtop  22871  tgqtop  22872  qtoprest  22877  kqsat  22891  kqcldsat  22893  kqnrmlem1  22903  kqnrmlem2  22904  hmeontr  22929  reghmph  22953  nrmhmph  22954  fmfnfmlem4  23117  fmfnfm  23118  flimopn  23135  flimclslem  23144  flfnei  23151  lmflf  23165  txflf  23166  fclsopn  23174  fclsfnflim  23187  alexsublem  23204  ptcmplem3  23214  cnextcn  23227  efmndtmd  23261  submtmd  23264  subgtgp  23265  symgtgp  23266  clssubg  23269  clsnsg  23270  tgpconncompeqg  23272  snclseqg  23276  tsmscls  23298  trust  23390  restutop  23398  restutopopn  23399  utop3cls  23412  utopreg  23413  trcfilu  23455  blssec  23597  prdsbl  23656  blssopn  23660  metcnp  23706  cfilucfil  23724  psmetutop  23732  iccntr  23993  icccmplem2  23995  reconnlem1  23998  metnrmlem1a  24030  metnrmlem1  24031  metnrmlem2  24032  metnrmlem3  24033  cnheibor  24127  lebnumlem1  24133  lebnumlem3  24135  lebnumii  24138  clsocv  24423  iscfil2  24439  iscmet3  24466  cmetss  24489  relcmpcmet  24491  bcthlem5  24501  itg1addlem5  24874  perfdvf  25076  dvres3  25086  dvres3a  25087  dvcmul  25117  dvcmulf  25118  dvlip2  25168  lhop1lem  25186  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcnvre  25192  dvcvx  25193  plyco0  25362  plyaddlem1  25383  plymullem1  25384  aalioulem3  25503  ulmdvlem1  25568  axcontlem10  27350  eengtrkg  27363  wlkp1lem7  28056  1wlkdlem4  28513  hsupunss  29714  pjpjpre  29790  ssmd2  30683  superpos  30725  atexch  30752  curry2ima  31050  pfxf1  31225  gsumhashmul  31325  symgcom2  31362  pmtrcnelor  31369  cycpmco2lem7  31408  cycpmconjvlem  31417  cycpmconjv  31418  cyc3conja  31433  nsgmgc  31606  nsgqusf1olem3  31609  elrspunidl  31615  mxidlprm  31649  lssdimle  31700  dimkerim  31717  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  madjusmdetlem2  31787  zarclsun  31829  rhmpreimacnlem  31843  ordtconnlem1  31883  measiuns  32194  imambfm  32238  cnmbfm  32239  dya2iocnrect  32257  omsfval  32270  omssubaddlem  32275  omssubadd  32276  totprobd  32402  fzssfzo  32527  signstfvn  32557  bnj999  32947  bnj1408  33025  bnj1442  33038  bnj1450  33039  bnj1501  33056  fnrelpredd  33070  revwlk  33095  cvmsss2  33245  cvmliftmolem1  33252  cvmliftlem3  33258  cvmlift2lem9  33282  cvmlift2lem11  33284  cvmlift3lem6  33295  cvmlift3lem7  33296  ssmclslem  33536  mclsax  33540  mclsppslem  33554  mclspps  33555  dfrdg2  33780  neiin  34530  neibastop2  34559  filnetlem4  34579  rdgssun  35558  lindsdom  35780  poimirlem11  35797  poimirlem12  35798  itg2addnclem2  35838  cnres2  35930  sstotbnd2  35941  sstotbnd  35942  prdstotbnd  35961  heibor1lem  35976  igenval2  36233  lshpnelb  37005  lcvexchlem4  37058  lsatexch  37064  l1cvat  37076  lkrscss  37119  lkrss  37189  lkreqN  37191  paddunN  37948  osumcllem2N  37978  pmapojoinN  37989  pl42lem2N  38001  dibglbN  39187  diblss  39191  dicvaddcl  39211  dicvscacl  39212  diclss  39214  cdlemn5pre  39221  dihord5apre  39283  dihglblem3N  39316  dihglb2  39363  dochsat  39404  dochshpncl  39405  djhspss  39427  dihsumssj  39429  mapdlsm  39685  hdmaprnlem3eN  39879  hdmaplkr  39934  fnwe2lem2  40883  lnmlsslnm  40913  lmhmfgima  40916  hbtlem6  40961  trrelsuperreldg  41283  iunrelexpuztr  41334  clsk1indlem2  41659  grumnudlem  41910  dvsconst  41955  dvsinax  43461  dvbdfbdioolem1  43476  itgsinexplem1  43502  itgperiod  43529  stoweidlem39  43587  dirkeritg  43650  fourierdlem48  43702  fourierdlem49  43703  fourierdlem70  43724  fourierdlem71  43725  fourierdlem81  43735  issalgend  43884  f1oresf1o  44793  subsubmgm  45362  rmsuppss  45717  restcls2lem  46217  iscnrm3rlem7  46251
  Copyright terms: Public domain W3C validator