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

Theorem sseqtrd 3603
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 3595 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 220 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  sseqtr4d  3604  uniintsn  4443  oeeui  7547  nnaword2  7575  oaabs2  7590  erssxp  7630  fipwuni  8193  ordtypelem7  8290  cantnflem3  8449  cdainf  8875  ficardun2  8886  ackbij1lem12  8914  ackbij1b  8922  fin1a2lem13  9095  winafp  9376  ioodisj  12132  reltrclfv  13555  prodss  14465  vdwlem11  15482  mrcssv  16046  mrcsscl  16052  mrcuni  16053  mressmrcd  16059  mreexexlem2d  16077  mreexexlem3d  16078  mreexfidimd  16083  subcss2  16275  resssetc  16514  funcsetcres2  16515  estrres  16551  poslubdg  16921  ipodrsfi  16935  acsmap2d  16951  mrelatlub  16958  mreclatBAD  16959  subsubm  17129  subsubg  17389  oppglsm  17829  subglsm  17858  lsmdisj  17866  gsumval3  18080  dprdres  18199  dprdss  18200  dprd2da  18213  dmdprdsplit2lem  18216  ablfac1b  18241  pgpfac1lem3  18248  issubdrg  18577  subsubrg  18578  islssd  18706  lspun  18757  lspssp  18758  lsslsp  18785  lsmssspx  18858  lspabs2  18890  lspabs3  18891  lspsolvlem  18912  lbsextlem3  18930  mplbas2  19240  gsumply1subr  19374  qsssubdrg  19573  obselocv  19839  lsslindf  19936  tgcl  20532  basgen  20551  tgfiss  20554  bastop1  20556  bastop2  20557  clsss2  20634  elcls3  20645  topssnei  20686  neiptopnei  20694  neitr  20742  restcls  20743  restlp  20745  ordtrest2  20766  iscncl  20831  cncls2  20835  cncls  20836  cnntr  20837  lmcls  20864  tgcmp  20962  cmpcld  20963  uncmp  20964  hauscmplem  20967  cmpfi  20969  clscon  20991  2ndcsb  21010  2ndcctbss  21016  2ndcomap  21019  nllyrest  21047  1stckgenlem  21114  kgencn2  21118  kgen2cn  21120  ptbasfi  21142  txcld  21164  txcls  21165  txbasval  21167  neitx  21168  ptcld  21174  ptclsg  21176  txnlly  21198  hausdiag  21206  txkgen  21213  xkopt  21216  xkopjcn  21217  xkococnlem  21220  cnmpt1res  21237  cnmpt2res  21238  imasnopn  21251  imasncld  21252  imasncls  21253  qtopcld  21274  qtoprest  21278  qtopcmap  21280  kqcldsat  21294  kqreglem2  21303  kqnrmlem2  21305  hmeontr  21330  neifil  21442  fgtr  21452  trnei  21454  uffixfr  21485  uffix2  21486  uffixsn  21487  elflim  21533  flimclslem  21546  fclsopn  21576  fclscmpi  21591  fclscmp  21592  alexsubALTlem3  21611  alexsubALT  21613  ptcmplem3  21616  subgntr  21668  opnsubg  21669  clssubg  21670  clsnsg  21671  cldsubg  21672  tgpconcompeqg  21673  snclseqg  21677  tsmsgsum  21700  tsmsid  21701  tgptsmscld  21712  ustssco  21776  utop2nei  21812  utop3cls  21813  utopreg  21814  cnextucn  21865  ressprdsds  21934  lpbl  22066  met2ndci  22085  prdsxmslem2  22092  metustexhalf  22119  psmetutop  22130  tgioo  22355  metdstri  22410  metdseq0  22413  xlebnum  22520  clsocv  22802  metelcls  22856  cmetss  22866  relcmpcmet  22868  cmpcmet  22869  minveclem4a  22954  uniioovol  23098  uniioombllem3  23104  limcres  23401  dvbss  23416  perfdvf  23418  dvreslem  23424  dvres2lem  23425  dvcnp2  23434  dvaddbr  23452  dvmulbr  23453  dvcmulf  23459  dvcj  23464  dvnfre  23466  dvmptres2  23476  dvmptcmul  23478  dvmptntr  23485  dvlip2  23507  dvcnvrelem2  23530  ftc1cn  23555  taylfvallem1  23860  taylply2  23871  taylply  23872  dvtaylp  23873  dvntaylp  23874  dvntaylp0  23875  taylthlem1  23876  taylthlem2  23877  ulmdvlem3  23905  pserulm  23925  shsub2  27402  spanssoc  27426  shub2  27460  ococin  27485  ssjo  27524  chub2  27585  spanpr  27657  elnlfn  28005  mdslj1i  28396  mdslmd3i  28409  mdexchi  28412  chirredlem1  28467  atcvat3i  28473  mdsymlem1  28480  mdsymlem5  28484  imadifxp  28630  qtophaus  29065  locfinreflem  29069  fsumcvg4  29158  esum2d  29316  omsmon  29521  omssubadd  29523  carsggect  29541  carsgclctun  29544  sitgclg  29565  eulerpartlemgf  29602  cvmscld  30343  cvmliftmolem1  30351  cvmlift2lem9  30381  cvmlift2lem11  30383  cvmlift3lem6  30394  nodense  30922  opnregcld  31329  ivthALT  31334  neibastop2  31360  fnemeet1  31365  fnejoin1  31367  poimirlem11  32414  poimirlem12  32415  poimirlem30  32433  ftc1cnnc  32478  sstotbnd  32568  ssbnd  32581  heibor1lem  32602  heiborlem3  32606  heibor  32614  lsmsat  33137  lssats  33141  lcvexchlem3  33165  lsatcvat3  33181  lkrscss  33227  lkrpssN  33292  pmod1i  33976  pclbtwnN  34025  pclunN  34026  pclss2polN  34049  pcl0N  34050  sspmaplubN  34053  paddunN  34055  pnonsingN  34061  pclfinclN  34078  osumcllem4N  34087  dia2dimlem13  35207  dvhopellsm  35248  dvadiaN  35259  dicelval1stN  35319  dicelval2nd  35320  dihssxp  35383  dihvalrel  35410  dochsscl  35499  dihoml4  35508  dochnoncon  35522  dvh3dim3N  35580  lcfrlem2  35674  lcfrlem5  35677  lcfr  35716  lcdlsp  35752  mapdsn  35772  mapdlsm  35795  mapdpglem1  35803  mapdindp0  35850  hlhilocv  36091  rntrclfvOAI  36096  ismrcd1  36103  ismrcd2  36104  coeq0i  36158  hbtlem6  36542  rgspnval  36581  iocinico  36640  trclubNEW  36769  ntrk2imkb  37179  isotone1  37190  k0004ss3  37295  wessf1ornlem  38190  iccdifprioo  38413  cncfuni  38596  cncfiooicclem1  38603  dvresntr  38630  dvmptresicc  38633  itgsubsticclem  38691  fourierdlem42  38866  fourierdlem48  38871  fourierdlem49  38872  fourierdlem50  38873  qndenserrn  39019  prsal  39038  intsaluni  39047  sssalgen  39053  dfsalgen2  39059  sge0f1o  39099  sge0split  39126  ismeannd  39184  caragensspw  39223  caragendifcl  39228  carageniuncl  39237  caratheodorylem1  39240  hoicvrrex  39270  ovnssle  39275  ovn02  39282  ovnsubadd  39286  hoidmv1le  39308  ovnlecvr2  39324  ovncvr2  39325  isvonmbl  39352  vonmblss  39354  ovolval4lem2  39364  ovnovollem1  39370  ovnovollem2  39371  incsmf  39453  decsmf  39477  subsubmgm  41609
  Copyright terms: Public domain W3C validator