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

Theorem sseqtr4d 3675
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 2657 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 3674 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  syl5sseqr  3687  fnfvima  6536  wfrlem17  7476  oaordi  7671  omordi  7691  omlimcl  7703  oen0  7711  domunsncan  8101  f1opwfi  8311  cantnfle  8606  cantnflt  8607  cantnflem1d  8623  r1pwss  8685  rankxplim3  8782  acndom2  8915  fodomfi2  8921  cflm  9110  cflim2  9123  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  axdc2lem  9308  ttukeylem5  9373  wunex2  9598  ssfzunsn  12425  ccatass  13406  swrdval2  13465  swrdccatin12  13537  splfv2a  13553  revccat  13561  cshimadifsn  13621  cshimadifsn0  13622  rtrclreclem1  13842  rtrclreclem2  13843  sumrblem  14486  prodrblem  14703  dfphi2  15526  vdwlem1  15732  basprssdmsets  15972  imasaddfnlem  16235  imasaddvallem  16236  imasvscafn  16244  imasvscaval  16245  mreexexlem4d  16354  mreexfidimd  16358  sscpwex  16522  acsmap2d  17226  gsumress  17323  subsubm  17404  frmdsssubm  17445  frmdss2  17447  subsubg  17664  cntzmhm2  17818  cntzcmnf  18294  ablcntzd  18306  gsumzsubmcl  18364  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  subgdmdprd  18479  dprdcntz2  18483  dprd2da  18487  dmdprdsplit2lem  18490  ablfac1eu  18518  pgpfaclem1  18526  pgpfaclem2  18527  issubdrg  18853  subsubrg  18854  lmhmlsp  19097  lspsntri  19145  lspindpi  19180  lidldvgen  19303  opsrtoslem2  19533  gsumfsum  19861  mrccss  20086  frlmsslsp  20183  scmatsgrp1  20376  toponss  20779  ssntr  20910  elcls3  20935  toponmre  20945  neiptoptop  20983  neiptopnei  20984  neitr  21032  ordtbas  21044  ordtopn1  21046  ordtopn2  21047  iscnp3  21096  tgcn  21104  tgcnp  21105  ssidcn  21107  cnclsi  21124  cncls  21126  cncnp  21132  lmcld  21155  tgcmp  21252  cnconn  21273  connima  21276  clsconn  21281  conncompcld  21285  1stccnp  21313  kgentopon  21389  llycmpkgen2  21401  1stckgen  21405  kgencn2  21408  ptopn  21434  txcls  21455  ptpjcn  21462  ptclsg  21466  xkoccn  21470  txcnp  21471  ptcnplem  21472  txcmplem2  21493  xkoptsub  21505  xkopt  21506  xkoco2cn  21509  xkococnlem  21510  xkoinjcn  21538  imasnopn  21541  imasncld  21542  imasncls  21543  qtopkgen  21561  basqtop  21562  tgqtop  21563  qtoprest  21568  kqsat  21582  kqcldsat  21584  kqnrmlem1  21594  kqnrmlem2  21595  hmeontr  21620  reghmph  21644  nrmhmph  21645  fmfnfmlem4  21808  fmfnfm  21809  flimopn  21826  flimclslem  21835  flfnei  21842  lmflf  21856  txflf  21857  fclsopn  21865  fclsfnflim  21878  alexsublem  21895  ptcmplem3  21905  cnextcn  21918  symgtgp  21952  submtmd  21955  subgtgp  21956  clssubg  21959  clsnsg  21960  tgpconncompeqg  21962  snclseqg  21966  tsmscls  21988  trust  22080  restutop  22088  restutopopn  22089  utop3cls  22102  utopreg  22103  trcfilu  22145  blssec  22287  prdsbl  22343  blssopn  22347  metcnp  22393  cfilucfil  22411  psmetutop  22419  iccntr  22671  icccmplem2  22673  reconnlem1  22676  metnrmlem1a  22708  metnrmlem1  22709  metnrmlem2  22710  metnrmlem3  22711  cnheibor  22801  lebnumlem1  22807  lebnumlem3  22809  lebnumii  22812  clsocv  23095  iscfil2  23110  iscmet3  23137  cmetss  23159  relcmpcmet  23161  bcthlem5  23171  itg1addlem5  23512  perfdvf  23712  dvres3  23722  dvres3a  23723  dvcmul  23752  dvcmulf  23753  dvlip2  23803  lhop1lem  23821  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  dvcvx  23828  plyco0  23993  plyaddlem1  24014  plymullem1  24015  aalioulem3  24134  ulmdvlem1  24199  axcontlem10  25898  eengtrkg  25910  wlkp1lem7  26632  1wlkdlem4  27118  hsupunss  28330  pjpjpre  28406  ssmd2  29299  superpos  29341  atexch  29368  curry2ima  29614  madjusmdetlem2  30022  ordtconnlem1  30098  measiuns  30408  imambfm  30452  cnmbfm  30453  dya2iocnrect  30471  omsfval  30484  omssubaddlem  30489  omssubadd  30490  totprobd  30616  fzssfzo  30741  signstfvn  30774  bnj999  31153  bnj1408  31230  bnj1442  31243  bnj1450  31244  bnj1501  31261  cvmsss2  31382  cvmliftmolem1  31389  cvmliftlem3  31395  cvmlift2lem9  31419  cvmlift2lem11  31421  cvmlift3lem6  31432  cvmlift3lem7  31433  ssmclslem  31588  mclsax  31592  mclsppslem  31606  mclspps  31607  dfrdg2  31825  trpredtr  31854  frrlem11  31917  neiin  32452  neibastop2  32481  filnetlem4  32501  lindsdom  33533  poimirlem11  33550  poimirlem12  33551  itg2addnclem2  33592  cnres2  33692  sstotbnd2  33703  sstotbnd  33704  prdstotbnd  33723  heibor1lem  33738  igenval2  33995  lshpnelb  34589  lcvexchlem4  34642  lsatexch  34648  l1cvat  34660  lkrscss  34703  lkrss  34773  lkreqN  34775  paddunN  35531  osumcllem2N  35561  pmapojoinN  35572  pl42lem2N  35584  dibglbN  36772  diblss  36776  dicvaddcl  36796  dicvscacl  36797  diclss  36799  cdlemn5pre  36806  dihord5apre  36868  dihglblem3N  36901  dihglb2  36948  dochsat  36989  dochshpncl  36990  djhspss  37012  dihsumssj  37014  mapdlsm  37270  hdmaprnlem3eN  37467  hdmaplkr  37522  fnwe2lem2  37938  lnmlsslnm  37968  lmhmfgima  37971  hbtlem6  38016  trrelsuperreldg  38277  iunrelexpuztr  38328  clsk1indlem2  38657  funfvima2d  38786  dvsconst  38846  fnfvimad  39773  dvsinax  40445  dvbdfbdioolem1  40461  itgsinexplem1  40487  itgperiod  40515  stoweidlem39  40574  dirkeritg  40637  fourierdlem48  40689  fourierdlem49  40690  fourierdlem70  40711  fourierdlem71  40712  fourierdlem81  40722  issalgend  40874  pfxccatin12  41750  subsubmgm  42122  rmsuppss  42476
  Copyright terms: Public domain W3C validator