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

Theorem sseqtr4d 3627
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 2627 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 3626 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  syl5sseqr  3639  fnfvima  6461  wfrlem17  7391  oaordi  7586  omordi  7606  omlimcl  7618  oen0  7626  domunsncan  8020  f1opwfi  8230  cantnfle  8528  cantnflt  8529  cantnflem1d  8545  r1pwss  8607  rankxplim3  8704  acndom2  8837  fodomfi2  8843  cflm  9032  cflim2  9045  isf34lem5  9160  isf34lem7  9161  isf34lem6  9162  axdc2lem  9230  ttukeylem5  9295  wunex2  9520  ssfzunsn  12345  ccatass  13326  swrdval2  13374  swrdccatin12  13444  splfv2a  13460  revccat  13468  cshimadifsn  13528  cshimadifsn0  13529  rtrclreclem1  13748  rtrclreclem2  13749  sumrblem  14391  prodrblem  14603  dfphi2  15422  vdwlem1  15628  basprssdmsets  15865  imasaddfnlem  16128  imasaddvallem  16129  imasvscafn  16137  imasvscaval  16138  mreexexlem4d  16247  mreexfidimd  16251  sscpwex  16415  acsmap2d  17119  gsumress  17216  subsubm  17297  frmdsssubm  17338  frmdss2  17340  subsubg  17557  cntzmhm2  17712  cntzcmnf  18188  ablcntzd  18200  gsumzsubmcl  18258  gsumconst  18274  gsumzmhm  18277  gsumzoppg  18284  subgdmdprd  18373  dprdcntz2  18377  dprd2da  18381  dmdprdsplit2lem  18384  ablfac1eu  18412  pgpfaclem1  18420  pgpfaclem2  18421  issubdrg  18745  subsubrg  18746  lmhmlsp  18989  lspsntri  19037  lspindpi  19072  lidldvgen  19195  opsrtoslem2  19425  gsumfsum  19753  mrccss  19978  frlmsslsp  20075  scmatsgrp1  20268  toponss  20671  ssntr  20802  elcls3  20827  toponmre  20837  neiptoptop  20875  neiptopnei  20876  neitr  20924  ordtbas  20936  ordtopn1  20938  ordtopn2  20939  iscnp3  20988  tgcn  20996  tgcnp  20997  ssidcn  20999  cnclsi  21016  cncls  21018  cncnp  21024  lmcld  21047  tgcmp  21144  cnconn  21165  connima  21168  clsconn  21173  conncompcld  21177  1stccnp  21205  kgentopon  21281  llycmpkgen2  21293  1stckgen  21297  kgencn2  21300  ptopn  21326  txcls  21347  ptpjcn  21354  ptclsg  21358  xkoccn  21362  txcnp  21363  ptcnplem  21364  txcmplem2  21385  xkoptsub  21397  xkopt  21398  xkoco2cn  21401  xkococnlem  21402  xkoinjcn  21430  imasnopn  21433  imasncld  21434  imasncls  21435  qtopkgen  21453  basqtop  21454  tgqtop  21455  qtoprest  21460  kqsat  21474  kqcldsat  21476  kqnrmlem1  21486  kqnrmlem2  21487  hmeontr  21512  reghmph  21536  nrmhmph  21537  fmfnfmlem4  21701  fmfnfm  21702  flimopn  21719  flimclslem  21728  flfnei  21735  lmflf  21749  txflf  21750  fclsopn  21758  fclsfnflim  21771  alexsublem  21788  ptcmplem3  21798  cnextcn  21811  symgtgp  21845  submtmd  21848  subgtgp  21849  clssubg  21852  clsnsg  21853  tgpconncompeqg  21855  snclseqg  21859  tsmscls  21881  trust  21973  restutop  21981  restutopopn  21982  utop3cls  21995  utopreg  21996  trcfilu  22038  blssec  22180  prdsbl  22236  blssopn  22240  metcnp  22286  cfilucfil  22304  psmetutop  22312  iccntr  22564  icccmplem2  22566  reconnlem1  22569  metnrmlem1a  22601  metnrmlem1  22602  metnrmlem2  22603  metnrmlem3  22604  cnheibor  22694  lebnumlem1  22700  lebnumlem3  22702  lebnumii  22705  clsocv  22989  iscfil2  23004  iscmet3  23031  cmetss  23053  relcmpcmet  23055  bcthlem5  23065  itg1addlem5  23407  perfdvf  23607  dvres3  23617  dvres3a  23618  dvcmul  23647  dvcmulf  23648  dvlip2  23696  lhop1lem  23714  dvcnvrelem1  23718  dvcnvrelem2  23719  dvcnvre  23720  dvcvx  23721  plyco0  23886  plyaddlem1  23907  plymullem1  23908  aalioulem3  24027  ulmdvlem1  24092  axcontlem10  25787  eengtrkg  25799  nbupgruvtxres  26229  wlkp1lem7  26479  1wlkdlem4  26900  hsupunss  28090  pjpjpre  28166  ssmd2  29059  superpos  29101  atexch  29128  curry2ima  29370  madjusmdetlem2  29718  ordtconnlem1  29794  measiuns  30103  imambfm  30147  cnmbfm  30148  dya2iocnrect  30166  omsfval  30179  omssubaddlem  30184  omssubadd  30185  totprobd  30311  fzssfzo  30436  signstfvn  30468  bnj999  30788  bnj1408  30865  bnj1442  30878  bnj1450  30879  bnj1501  30896  cvmsss2  31017  cvmliftmolem1  31024  cvmliftlem3  31030  cvmlift2lem9  31054  cvmlift2lem11  31056  cvmlift3lem6  31067  cvmlift3lem7  31068  ssmclslem  31223  mclsax  31227  mclsppslem  31241  mclspps  31242  dfrdg2  31455  trpredtr  31484  neiin  32022  neibastop2  32051  filnetlem4  32071  lindsdom  33074  poimirlem11  33091  poimirlem12  33092  itg2addnclem2  33133  cnres2  33233  sstotbnd2  33244  sstotbnd  33245  prdstotbnd  33264  heibor1lem  33279  igenval2  33536  lshpnelb  33790  lcvexchlem4  33843  lsatexch  33849  l1cvat  33861  lkrscss  33904  lkrss  33974  lkreqN  33976  paddunN  34732  osumcllem2N  34762  pmapojoinN  34773  pl42lem2N  34785  dibglbN  35974  diblss  35978  dicvaddcl  35998  dicvscacl  35999  diclss  36001  cdlemn5pre  36008  dihord5apre  36070  dihglblem3N  36103  dihglb2  36150  dochsat  36191  dochshpncl  36192  djhspss  36214  dihsumssj  36216  mapdlsm  36472  hdmaprnlem3eN  36669  hdmaplkr  36724  fnwe2lem2  37140  lnmlsslnm  37170  lmhmfgima  37173  hbtlem6  37219  trrelsuperreldg  37480  iunrelexpuztr  37531  clsk1indlem2  37861  funfvima2d  37990  dvsconst  38050  fnfvimad  38969  dvsinax  39463  dvbdfbdioolem1  39480  itgsinexplem1  39506  itgperiod  39534  stoweidlem39  39593  dirkeritg  39656  fourierdlem48  39708  fourierdlem49  39709  fourierdlem70  39730  fourierdlem71  39731  fourierdlem81  39741  issalgend  39893  pfxccatin12  40754  subsubmgm  41115  rmsuppss  41469
  Copyright terms: Public domain W3C validator