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

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

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2 (𝜑𝐴𝐵)
2 sseqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32sseq2d 3666 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 222 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:  sseqtr4d  3675  uniintsn  4546  oeeui  7727  nnaword2  7755  oaabs2  7770  erssxp  7810  fipwuni  8373  ordtypelem7  8470  cantnflem3  8626  cdainf  9052  ficardun2  9063  ackbij1lem12  9091  ackbij1b  9099  fin1a2lem13  9272  winafp  9557  ioodisj  12340  reltrclfv  13802  prodss  14721  vdwlem11  15742  mrcssv  16321  mrcsscl  16327  mrcuni  16328  mressmrcd  16334  mreexexlem2d  16352  mreexexlem3d  16353  mreexfidimd  16358  subcss2  16550  resssetc  16789  funcsetcres2  16790  estrres  16826  poslubdg  17196  ipodrsfi  17210  acsmap2d  17226  mrelatlub  17233  mreclatBAD  17234  subsubm  17404  subsubg  17664  oppglsm  18103  subglsm  18132  lsmdisj  18140  gsumval3  18354  dprdres  18473  dprdss  18474  dprd2da  18487  dmdprdsplit2lem  18490  ablfac1b  18515  pgpfac1lem3  18522  issubdrg  18853  subsubrg  18854  islssd  18984  lspun  19035  lspssp  19036  lsslsp  19063  lsmssspx  19136  lspabs2  19168  lspabs3  19169  lspsolvlem  19190  lbsextlem3  19208  mplbas2  19518  gsumply1subr  19652  qsssubdrg  19853  obselocv  20120  lsslindf  20217  tgcl  20821  basgen  20840  tgfiss  20843  bastop1  20845  bastop2  20846  clsss2  20924  elcls3  20935  topssnei  20976  neiptopnei  20984  neitr  21032  restcls  21033  restlp  21035  ordtrest2  21056  iscncl  21121  cncls2  21125  cncls  21126  cnntr  21127  lmcls  21154  tgcmp  21252  cmpcld  21253  uncmp  21254  hauscmplem  21257  cmpfi  21259  clsconn  21281  2ndcsb  21300  2ndcctbss  21306  2ndcomap  21309  nllyrest  21337  1stckgenlem  21404  kgencn2  21408  kgen2cn  21410  ptbasfi  21432  txcld  21454  txcls  21455  txbasval  21457  neitx  21458  ptcld  21464  ptclsg  21466  txnlly  21488  hausdiag  21496  txkgen  21503  xkopt  21506  xkopjcn  21507  xkococnlem  21510  cnmpt1res  21527  cnmpt2res  21528  imasnopn  21541  imasncld  21542  imasncls  21543  qtopcld  21564  qtoprest  21568  qtopcmap  21570  kqcldsat  21584  kqreglem2  21593  kqnrmlem2  21595  hmeontr  21620  neifil  21731  fgtr  21741  trnei  21743  uffixfr  21774  uffix2  21775  uffixsn  21776  elflim  21822  flimclslem  21835  fclsopn  21865  fclscmpi  21880  fclscmp  21881  alexsubALTlem3  21900  alexsubALT  21902  ptcmplem3  21905  subgntr  21957  opnsubg  21958  clssubg  21959  clsnsg  21960  cldsubg  21961  tgpconncompeqg  21962  snclseqg  21966  tsmsgsum  21989  tsmsid  21990  tgptsmscld  22001  ustssco  22065  utop2nei  22101  utop3cls  22102  utopreg  22103  cnextucn  22154  ressprdsds  22223  lpbl  22355  met2ndci  22374  prdsxmslem2  22381  metustexhalf  22408  psmetutop  22419  tgioo  22646  metdstri  22701  metdseq0  22704  xlebnum  22811  clsocv  23095  metelcls  23149  cmetss  23159  relcmpcmet  23161  cmpcmet  23162  minveclem4a  23247  uniioovol  23393  uniioombllem3  23399  limcres  23695  dvbss  23710  perfdvf  23712  dvreslem  23718  dvres2lem  23719  dvcnp2  23728  dvaddbr  23746  dvmulbr  23747  dvcmulf  23753  dvcj  23758  dvnfre  23760  dvmptres2  23770  dvmptcmul  23772  dvmptntr  23779  dvlip2  23803  dvcnvrelem2  23826  ftc1cn  23851  taylfvallem1  24156  taylply2  24167  taylply  24168  dvtaylp  24169  dvntaylp  24170  dvntaylp0  24171  taylthlem1  24172  taylthlem2  24173  ulmdvlem3  24201  pserulm  24221  shsub2  28312  spanssoc  28336  shub2  28370  ococin  28395  ssjo  28434  chub2  28495  spanpr  28567  elnlfn  28915  mdslj1i  29306  mdslmd3i  29319  mdexchi  29322  chirredlem1  29377  atcvat3i  29383  mdsymlem1  29390  mdsymlem5  29394  imadifxp  29540  qtophaus  30031  locfinreflem  30035  fsumcvg4  30124  esum2d  30283  omsmon  30488  omssubadd  30490  carsggect  30508  carsgclctun  30511  sitgclg  30532  eulerpartlemgf  30569  reprpmtf1o  30832  cvmscld  31381  cvmliftmolem1  31389  cvmlift2lem9  31419  cvmlift2lem11  31421  cvmlift3lem6  31432  nodense  31967  opnregcld  32450  ivthALT  32455  neibastop2  32481  fnemeet1  32486  fnejoin1  32488  poimirlem11  33550  poimirlem12  33551  poimirlem30  33569  ftc1cnnc  33614  sstotbnd  33704  ssbnd  33717  heibor1lem  33738  heiborlem3  33742  heibor  33750  lsmsat  34613  lssats  34617  lcvexchlem3  34641  lsatcvat3  34657  lkrscss  34703  lkrpssN  34768  pmod1i  35452  pclbtwnN  35501  pclunN  35502  pclss2polN  35525  pcl0N  35526  sspmaplubN  35529  paddunN  35531  pnonsingN  35537  pclfinclN  35554  osumcllem4N  35563  dia2dimlem13  36682  dvhopellsm  36723  dvadiaN  36734  dicelval1stN  36794  dicelval2nd  36795  dihssxp  36858  dihvalrel  36885  dochsscl  36974  dihoml4  36983  dochnoncon  36997  dvh3dim3N  37055  lcfrlem2  37149  lcfrlem5  37152  lcfr  37191  lcdlsp  37227  mapdsn  37247  mapdlsm  37270  mapdpglem1  37278  mapdindp0  37325  hlhilocv  37566  rntrclfvOAI  37571  ismrcd1  37578  ismrcd2  37579  coeq0i  37633  hbtlem6  38016  rgspnval  38055  iocinico  38114  trclubNEW  38243  ntrk2imkb  38652  isotone1  38663  k0004ss3  38768  wessf1ornlem  39685  iccdifprioo  40060  limsupequzmptlem  40278  cncfuni  40417  cncfiooicclem1  40424  dvresntr  40450  dvmptresicc  40452  itgsubsticclem  40509  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  qndenserrn  40837  prsal  40856  intsaluni  40865  sssalgen  40871  dfsalgen2  40877  sge0f1o  40917  sge0split  40944  ismeannd  41002  caragensspw  41044  caragendifcl  41049  carageniuncl  41058  caratheodorylem1  41061  hoicvrrex  41091  ovnssle  41096  ovn02  41103  ovnsubadd  41107  hoidmv1le  41129  ovnlecvr2  41145  ovncvr2  41146  isvonmbl  41173  vonmblss  41175  ovolval4lem2  41185  ovnovollem1  41191  ovnovollem2  41192  incsmf  41272  decsmf  41296  uspgropssxp  42077  subsubmgm  42122
  Copyright terms: Public domain W3C validator