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

Theorem sseqtr4d 3605
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 2616 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 3604 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  syl5sseqr  3617  fnfvima  6400  wfrlem17  7318  oaordi  7513  omordi  7533  omlimcl  7545  oen0  7553  domunsncan  7945  f1opwfi  8153  cantnfle  8451  cantnflt  8452  cantnflem1d  8468  r1pwss  8530  rankxplim3  8627  acndom2  8760  fodomfi2  8766  cflm  8955  cflim2  8968  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  axdc2lem  9153  ttukeylem5  9218  wunex2  9439  ccatass  13224  swrdval2  13272  swrdccatin12  13342  splfv2a  13358  revccat  13366  cshimadifsn  13426  cshimadifsn0  13427  rtrclreclem1  13646  rtrclreclem2  13647  sumrblem  14289  prodrblem  14498  dfphi2  15317  vdwlem1  15523  imasaddfnlem  16011  imasaddvallem  16012  imasvscafn  16020  imasvscaval  16021  mreexexlem4d  16130  mreexfidimd  16134  sscpwex  16298  acsmap2d  17002  gsumress  17099  subsubm  17180  frmdsssubm  17221  frmdss2  17223  subsubg  17440  cntzmhm2  17595  cntzcmnf  18071  ablcntzd  18083  gsumzsubmcl  18141  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  subgdmdprd  18256  dprdcntz2  18260  dprd2da  18264  dmdprdsplit2lem  18267  ablfac1eu  18295  pgpfaclem1  18303  pgpfaclem2  18304  issubdrg  18628  subsubrg  18629  lmhmlsp  18870  lspsntri  18918  lspindpi  18953  lidldvgen  19076  opsrtoslem2  19306  gsumfsum  19632  mrccss  19857  frlmsslsp  19954  scmatsgrp1  20147  toponss  20544  ssntr  20672  elcls3  20697  toponmre  20707  neiptoptop  20745  neiptopnei  20746  neitr  20794  ordtbas  20806  ordtopn1  20808  ordtopn2  20809  iscnp3  20858  tgcn  20866  tgcnp  20867  ssidcn  20869  cnclsi  20886  cncls  20888  cncnp  20894  lmcld  20917  tgcmp  21014  cnconn  21035  conima  21038  clscon  21043  concompcld  21047  1stccnp  21075  kgentopon  21151  llycmpkgen2  21163  1stckgen  21167  kgencn2  21170  ptopn  21196  txcls  21217  ptpjcn  21224  ptclsg  21228  xkoccn  21232  txcnp  21233  ptcnplem  21234  txcmplem2  21255  xkoptsub  21267  xkopt  21268  xkoco2cn  21271  xkococnlem  21272  xkoinjcn  21300  imasnopn  21303  imasncld  21304  imasncls  21305  qtopkgen  21323  basqtop  21324  tgqtop  21325  qtoprest  21330  kqsat  21344  kqcldsat  21346  kqnrmlem1  21356  kqnrmlem2  21357  hmeontr  21382  reghmph  21406  nrmhmph  21407  fmfnfmlem4  21571  fmfnfm  21572  flimopn  21589  flimclslem  21598  flfnei  21605  lmflf  21619  txflf  21620  fclsopn  21628  fclsfnflim  21641  alexsublem  21658  ptcmplem3  21668  cnextcn  21681  symgtgp  21715  submtmd  21718  subgtgp  21719  clssubg  21722  clsnsg  21723  tgpconcompeqg  21725  snclseqg  21729  tsmscls  21751  trust  21843  restutop  21851  restutopopn  21852  utop3cls  21865  utopreg  21866  trcfilu  21908  blssec  22050  prdsbl  22106  blssopn  22110  metcnp  22156  cfilucfil  22174  psmetutop  22182  iccntr  22432  icccmplem2  22434  reconnlem1  22437  metnrmlem1a  22469  metnrmlem1  22470  metnrmlem2  22471  metnrmlem3  22472  cnheibor  22562  lebnumlem1  22568  lebnumlem3  22570  lebnumii  22573  clsocv  22857  iscfil2  22872  iscmet3  22899  cmetss  22921  relcmpcmet  22923  bcthlem5  22933  itg1addlem5  23273  perfdvf  23473  dvres3  23483  dvres3a  23484  dvcmul  23513  dvcmulf  23514  dvlip2  23562  lhop1lem  23580  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvcvx  23587  plyco0  23752  plyaddlem1  23773  plymullem1  23774  aalioulem3  23893  ulmdvlem1  23958  axcontlem10  25653  eengtrkg  25665  uhgrstrrepelem  25744  eupares  26502  hsupunss  27586  pjpjpre  27662  ssmd2  28555  superpos  28597  atexch  28624  curry2ima  28869  madjusmdetlem2  29222  ordtconlem1  29298  measiuns  29607  imambfm  29651  cnmbfm  29652  dya2iocnrect  29670  omsfval  29683  omssubaddlem  29688  omssubadd  29689  totprobd  29815  fzssfzo  29940  signstfvn  29972  bnj999  30281  bnj1408  30358  bnj1442  30371  bnj1450  30372  bnj1501  30389  cvmsss2  30510  cvmliftmolem1  30517  cvmliftlem3  30523  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift3lem6  30560  cvmlift3lem7  30561  ssmclslem  30716  mclsax  30720  mclsppslem  30734  mclspps  30735  dfrdg2  30945  trpredtr  30974  neiin  31497  neibastop2  31526  filnetlem4  31546  lindsdom  32573  poimirlem11  32590  poimirlem12  32591  itg2addnclem2  32632  cnres2  32732  sstotbnd2  32743  sstotbnd  32744  prdstotbnd  32763  heibor1lem  32778  igenval2  33035  lshpnelb  33289  lcvexchlem4  33342  lsatexch  33348  l1cvat  33360  lkrscss  33403  lkrss  33473  lkreqN  33475  paddunN  34231  osumcllem2N  34261  pmapojoinN  34272  pl42lem2N  34284  dibglbN  35473  diblss  35477  dicvaddcl  35497  dicvscacl  35498  diclss  35500  cdlemn5pre  35507  dihord5apre  35569  dihglblem3N  35602  dihglb2  35649  dochsat  35690  dochshpncl  35691  djhspss  35713  dihsumssj  35715  mapdlsm  35971  hdmaprnlem3eN  36168  hdmaplkr  36223  fnwe2lem2  36639  lnmlsslnm  36669  lmhmfgima  36672  hbtlem6  36718  trrelsuperreldg  36979  iunrelexpuztr  37030  clsk1indlem2  37360  funfvima2d  37491  dvsconst  37551  dvsinax  38801  dvbdfbdioolem1  38818  itgsinexplem1  38845  itgperiod  38873  stoweidlem39  38932  dirkeritg  38995  fourierdlem48  39047  fourierdlem49  39048  fourierdlem70  39069  fourierdlem71  39070  fourierdlem81  39080  issalgend  39232  pfxccatin12  40288  nbupgruvtxres  40634  1wlkp1lem7  40888  11wlkdlem4  41307  subsubmgm  41587  rmsuppss  41945
  Copyright terms: Public domain W3C validator