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

Theorem sseqtrrd 4008
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 2827 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 4007 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wss 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952
This theorem is referenced by:  sseqtrrid  4020  funfvima2d  6988  fnfvima  6989  wfrlem17  7965  oaordi  8166  omordi  8186  omlimcl  8198  oen0  8206  domunsncan  8611  f1opwfi  8822  cantnfle  9128  cantnflt  9129  cantnflem1d  9145  r1pwss  9207  rankxplim3  9304  acndom2  9474  fodomfi2  9480  cflm  9666  cflim2  9679  isf34lem5  9794  isf34lem7  9795  isf34lem6  9796  axdc2lem  9864  ttukeylem5  9929  wunex2  10154  ssfzunsn  12947  ccatass  13936  swrdval2  14002  splfv2a  14112  revccat  14122  cshimadifsn  14185  cshimadifsn0  14186  rtrclreclem1  14411  rtrclreclem2  14412  sumrblem  15062  prodrblem  15277  dfphi2  16105  vdwlem1  16311  basprssdmsets  16543  imasaddfnlem  16795  imasaddvallem  16796  imasvscafn  16804  imasvscaval  16805  mreexexlem4d  16912  mreexfidimd  16915  sscpwex  17079  acsmap2d  17783  gsumress  17886  subsubm  17975  frmdsssubm  18020  frmdss2  18022  subsubg  18296  cntzmhm2  18464  cntzcmnf  18959  ablcntzd  18971  gsumzsubmcl  19032  gsumconst  19048  gsumzmhm  19051  subgdmdprd  19150  dprdcntz2  19154  dprd2da  19158  dmdprdsplit2lem  19161  ablfac1eu  19189  pgpfaclem1  19197  pgpfaclem2  19198  issubdrg  19554  subsubrg  19555  subdrgint  19576  lmhmlsp  19815  lspsntri  19863  lspindpi  19898  lidldvgen  20022  opsrtoslem2  20259  gsumfsum  20606  mrccss  20832  frlmsslsp  20934  scmatsgrp1  21125  toponss  21529  ssntr  21660  elcls3  21685  toponmre  21695  neiptoptop  21733  neiptopnei  21734  neitr  21782  ordtbas  21794  ordtopn1  21796  ordtopn2  21797  iscnp3  21846  tgcn  21854  tgcnp  21855  ssidcn  21857  cnclsi  21874  cncls  21876  cncnp  21882  lmcld  21905  tgcmp  22003  cnconn  22024  connima  22027  clsconn  22032  conncompcld  22036  1stccnp  22064  kgentopon  22140  llycmpkgen2  22152  1stckgen  22156  kgencn2  22159  ptopn  22185  txcls  22206  ptpjcn  22213  ptclsg  22217  xkoccn  22221  txcnp  22222  ptcnplem  22223  txcmplem2  22244  xkoptsub  22256  xkopt  22257  xkoco2cn  22260  xkococnlem  22261  xkoinjcn  22289  imasnopn  22292  imasncld  22293  imasncls  22294  qtopkgen  22312  basqtop  22313  tgqtop  22314  qtoprest  22319  kqsat  22333  kqcldsat  22335  kqnrmlem1  22345  kqnrmlem2  22346  hmeontr  22371  reghmph  22395  nrmhmph  22396  fmfnfmlem4  22559  fmfnfm  22560  flimopn  22577  flimclslem  22586  flfnei  22593  lmflf  22607  txflf  22608  fclsopn  22616  fclsfnflim  22629  alexsublem  22646  ptcmplem3  22656  cnextcn  22669  efmndtmd  22703  submtmd  22706  subgtgp  22707  symgtgp  22708  clssubg  22711  clsnsg  22712  tgpconncompeqg  22714  snclseqg  22718  tsmscls  22740  trust  22832  restutop  22840  restutopopn  22841  utop3cls  22854  utopreg  22855  trcfilu  22897  blssec  23039  prdsbl  23095  blssopn  23099  metcnp  23145  cfilucfil  23163  psmetutop  23171  iccntr  23423  icccmplem2  23425  reconnlem1  23428  metnrmlem1a  23460  metnrmlem1  23461  metnrmlem2  23462  metnrmlem3  23463  cnheibor  23553  lebnumlem1  23559  lebnumlem3  23561  lebnumii  23564  clsocv  23847  iscfil2  23863  iscmet3  23890  cmetss  23913  relcmpcmet  23915  bcthlem5  23925  itg1addlem5  24295  perfdvf  24495  dvres3  24505  dvres3a  24506  dvcmul  24535  dvcmulf  24536  dvlip2  24586  lhop1lem  24604  dvcnvrelem1  24608  dvcnvrelem2  24609  dvcnvre  24610  dvcvx  24611  plyco0  24776  plyaddlem1  24797  plymullem1  24798  aalioulem3  24917  ulmdvlem1  24982  axcontlem10  26753  eengtrkg  26766  wlkp1lem7  27455  1wlkdlem4  27913  hsupunss  29114  pjpjpre  29190  ssmd2  30083  superpos  30125  atexch  30152  curry2ima  30438  pfxf1  30613  symgcom2  30723  pmtrcnelor  30730  cycpmco2lem7  30769  cycpmconjvlem  30778  cycpmconjv  30779  cyc3conja  30794  mxidlprm  30972  lssdimle  31001  dimkerim  31018  fedgmullem1  31020  fedgmullem2  31021  fedgmul  31022  madjusmdetlem2  31088  ordtconnlem1  31162  measiuns  31471  imambfm  31515  cnmbfm  31516  dya2iocnrect  31534  omsfval  31547  omssubaddlem  31552  omssubadd  31553  totprobd  31679  fzssfzo  31804  signstfvn  31834  bnj999  32225  bnj1408  32303  bnj1442  32316  bnj1450  32317  bnj1501  32334  revwlk  32366  cvmsss2  32516  cvmliftmolem1  32523  cvmliftlem3  32529  cvmlift2lem9  32553  cvmlift2lem11  32555  cvmlift3lem6  32566  cvmlift3lem7  32567  ssmclslem  32807  mclsax  32811  mclsppslem  32825  mclspps  32826  dfrdg2  33035  trpredtr  33064  frrlem8  33125  frrlem10  33127  neiin  33675  neibastop2  33704  filnetlem4  33724  rdgssun  34653  lindsdom  34880  poimirlem11  34897  poimirlem12  34898  itg2addnclem2  34938  cnres2  35035  sstotbnd2  35046  sstotbnd  35047  prdstotbnd  35066  heibor1lem  35081  igenval2  35338  lshpnelb  36114  lcvexchlem4  36167  lsatexch  36173  l1cvat  36185  lkrscss  36228  lkrss  36298  lkreqN  36300  paddunN  37057  osumcllem2N  37087  pmapojoinN  37098  pl42lem2N  37110  dibglbN  38296  diblss  38300  dicvaddcl  38320  dicvscacl  38321  diclss  38323  cdlemn5pre  38330  dihord5apre  38392  dihglblem3N  38425  dihglb2  38472  dochsat  38513  dochshpncl  38514  djhspss  38536  dihsumssj  38538  mapdlsm  38794  hdmaprnlem3eN  38988  hdmaplkr  39043  fnwe2lem2  39644  lnmlsslnm  39674  lmhmfgima  39677  hbtlem6  39722  trrelsuperreldg  40006  iunrelexpuztr  40057  clsk1indlem2  40385  grumnudlem  40614  dvsconst  40655  dvsinax  42189  dvbdfbdioolem1  42205  itgsinexplem1  42231  itgperiod  42258  stoweidlem39  42317  dirkeritg  42380  fourierdlem48  42432  fourierdlem49  42433  fourierdlem70  42454  fourierdlem71  42455  fourierdlem81  42465  issalgend  42614  f1oresf1o  43482  subsubmgm  44057  rmsuppss  44411
  Copyright terms: Public domain W3C validator