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

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

Proof of Theorem sseqtr4d
StepHypRef Expression
1 sseqtr4d.1 . 2 (𝜑𝐴𝐵)
2 sseqtr4d.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2819 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 3845 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-in 3783  df-ss 3790
This theorem is referenced by:  syl5sseqr  3858  fnfvima  6724  wfrlem17  7670  oaordi  7866  omordi  7886  omlimcl  7898  oen0  7906  domunsncan  8302  f1opwfi  8512  cantnfle  8818  cantnflt  8819  cantnflem1d  8835  r1pwss  8897  rankxplim3  8994  acndom2  9163  fodomfi2  9169  cflm  9360  cflim2  9373  isf34lem5  9488  isf34lem7  9489  isf34lem6  9490  axdc2lem  9558  ttukeylem5  9623  wunex2  9848  ssfzunsn  12613  ccatass  13588  swrdval2  13646  swrdccatin12  13718  splfv2a  13734  revccat  13742  cshimadifsn  13802  cshimadifsn0  13803  rtrclreclem1  14024  rtrclreclem2  14025  sumrblem  14668  prodrblem  14883  dfphi2  15699  vdwlem1  15905  basprssdmsets  16139  imasaddfnlem  16396  imasaddvallem  16397  imasvscafn  16405  imasvscaval  16406  mreexexlem4d  16515  mreexfidimd  16518  sscpwex  16682  acsmap2d  17387  gsumress  17484  subsubm  17565  frmdsssubm  17606  frmdss2  17608  subsubg  17822  cntzmhm2  17976  cntzcmnf  18452  ablcntzd  18464  gsumzsubmcl  18522  gsumconst  18538  gsumzmhm  18541  subgdmdprd  18638  dprdcntz2  18642  dprd2da  18646  dmdprdsplit2lem  18649  ablfac1eu  18677  pgpfaclem1  18685  pgpfaclem2  18686  issubdrg  19012  subsubrg  19013  lmhmlsp  19259  lspsntri  19307  lspindpi  19343  lidldvgen  19467  opsrtoslem2  19696  gsumfsum  20024  mrccss  20252  frlmsslsp  20349  scmatsgrp1  20543  toponss  20949  ssntr  21080  elcls3  21105  toponmre  21115  neiptoptop  21153  neiptopnei  21154  neitr  21202  ordtbas  21214  ordtopn1  21216  ordtopn2  21217  iscnp3  21266  tgcn  21274  tgcnp  21275  ssidcn  21277  cnclsi  21294  cncls  21296  cncnp  21302  lmcld  21325  tgcmp  21422  cnconn  21443  connima  21446  clsconn  21451  conncompcld  21455  1stccnp  21483  kgentopon  21559  llycmpkgen2  21571  1stckgen  21575  kgencn2  21578  ptopn  21604  txcls  21625  ptpjcn  21632  ptclsg  21636  xkoccn  21640  txcnp  21641  ptcnplem  21642  txcmplem2  21663  xkoptsub  21675  xkopt  21676  xkoco2cn  21679  xkococnlem  21680  xkoinjcn  21708  imasnopn  21711  imasncld  21712  imasncls  21713  qtopkgen  21731  basqtop  21732  tgqtop  21733  qtoprest  21738  kqsat  21752  kqcldsat  21754  kqnrmlem1  21764  kqnrmlem2  21765  hmeontr  21790  reghmph  21814  nrmhmph  21815  fmfnfmlem4  21978  fmfnfm  21979  flimopn  21996  flimclslem  22005  flfnei  22012  lmflf  22026  txflf  22027  fclsopn  22035  fclsfnflim  22048  alexsublem  22065  ptcmplem3  22075  cnextcn  22088  symgtgp  22122  submtmd  22125  subgtgp  22126  clssubg  22129  clsnsg  22130  tgpconncompeqg  22132  snclseqg  22136  tsmscls  22158  trust  22250  restutop  22258  restutopopn  22259  utop3cls  22272  utopreg  22273  trcfilu  22315  blssec  22457  prdsbl  22513  blssopn  22517  metcnp  22563  cfilucfil  22581  psmetutop  22589  iccntr  22841  icccmplem2  22843  reconnlem1  22846  metnrmlem1a  22878  metnrmlem1  22879  metnrmlem2  22880  metnrmlem3  22881  cnheibor  22971  lebnumlem1  22977  lebnumlem3  22979  lebnumii  22982  clsocv  23265  iscfil2  23281  iscmet3  23308  cmetss  23330  relcmpcmet  23332  bcthlem5  23342  itg1addlem5  23687  perfdvf  23887  dvres3  23897  dvres3a  23898  dvcmul  23927  dvcmulf  23928  dvlip2  23978  lhop1lem  23996  dvcnvrelem1  24000  dvcnvrelem2  24001  dvcnvre  24002  dvcvx  24003  plyco0  24168  plyaddlem1  24189  plymullem1  24190  aalioulem3  24309  ulmdvlem1  24374  axcontlem10  26073  eengtrkg  26085  wlkp1lem7  26810  1wlkdlem4  27319  hsupunss  28536  pjpjpre  28612  ssmd2  29505  superpos  29547  atexch  29574  curry2ima  29819  madjusmdetlem2  30225  ordtconnlem1  30301  measiuns  30611  imambfm  30655  cnmbfm  30656  dya2iocnrect  30674  omsfval  30687  omssubaddlem  30692  omssubadd  30693  totprobd  30819  fzssfzo  30944  signstfvn  30977  bnj999  31355  bnj1408  31432  bnj1442  31445  bnj1450  31446  bnj1501  31463  cvmsss2  31584  cvmliftmolem1  31591  cvmliftlem3  31597  cvmlift2lem9  31621  cvmlift2lem11  31623  cvmlift3lem6  31634  cvmlift3lem7  31635  ssmclslem  31790  mclsax  31794  mclsppslem  31808  mclspps  31809  dfrdg2  32026  trpredtr  32055  frrlem11  32118  neiin  32653  neibastop2  32682  filnetlem4  32702  lindsdom  33718  poimirlem11  33735  poimirlem12  33736  itg2addnclem2  33776  cnres2  33875  sstotbnd2  33886  sstotbnd  33887  prdstotbnd  33906  heibor1lem  33921  igenval2  34178  lshpnelb  34766  lcvexchlem4  34819  lsatexch  34825  l1cvat  34837  lkrscss  34880  lkrss  34950  lkreqN  34952  paddunN  35709  osumcllem2N  35739  pmapojoinN  35750  pl42lem2N  35762  dibglbN  36948  diblss  36952  dicvaddcl  36972  dicvscacl  36973  diclss  36975  cdlemn5pre  36982  dihord5apre  37044  dihglblem3N  37077  dihglb2  37124  dochsat  37165  dochshpncl  37166  djhspss  37188  dihsumssj  37190  mapdlsm  37446  hdmaprnlem3eN  37640  hdmaplkr  37695  fnwe2lem2  38123  lnmlsslnm  38153  lmhmfgima  38156  hbtlem6  38201  trrelsuperreldg  38461  iunrelexpuztr  38512  clsk1indlem2  38841  funfvima2d  38970  dvsconst  39030  fnfvimad  39944  dvsinax  40608  dvbdfbdioolem1  40624  itgsinexplem1  40650  itgperiod  40677  stoweidlem39  40736  dirkeritg  40799  fourierdlem48  40851  fourierdlem49  40852  fourierdlem70  40873  fourierdlem71  40874  fourierdlem81  40884  issalgend  41036  f1oresf1o  41881  f1oresf1o2  41882  pfxccatin12  42001  subsubmgm  42366  rmsuppss  42720
  Copyright terms: Public domain W3C validator