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

Theorem eqsstrid 4018
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstrid.1 𝐴 = 𝐵
eqsstrid.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqsstrid (𝜑𝐴𝐶)

Proof of Theorem eqsstrid
StepHypRef Expression
1 eqsstrid.2 . 2 (𝜑𝐵𝐶)
2 eqsstrid.1 . . 3 𝐴 = 𝐵
32sseq1i 3998 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 236 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1536  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-in 3946  df-ss 3955
This theorem is referenced by:  eqsstrrid  4019  inss  4218  tpssi  4772  xpsspw  5685  opabssxpd  5792  fun  6543  fmpt  6877  fliftrel  7064  knatar  7113  fr3nr  7497  suceloni  7531  fiun  7647  f1iun  7648  1stcof  7722  2ndcof  7723  fsplitfpar  7817  fnwelem  7828  oeeui  8231  aceq3lem  9549  cflecard  9678  cfslb2n  9693  itunitc1  9845  axdc3lem2  9876  fpwwe2lem12  10066  canthwelem  10075  wuncval2  10172  peano5nni  11644  un0addcl  11933  un0mulcl  11934  fsuppmapnn0fiublem  13361  fsuppmapnn0fiub  13362  mertenslem2  15244  4sqlem11  16294  4sqlem19  16302  vdwlem13  16332  imasless  16816  rescfth  17210  oppchofcl  17513  oyoncl  17523  mgmidsssn0  17885  cycsubm  18348  efgsfo  18868  efgcpbllemb  18884  frgpuplem  18901  gsummpt1n0  19088  dprdfid  19142  dprd2d2  19169  ablfacrp  19191  ablfac1b  19195  ablfac1eu  19198  pgpfac1lem5  19204  ablfaclem3  19212  lsptpcl  19754  lsppratlem3  19924  lsppratlem4  19925  lbsextlem2  19934  f1lindf  20969  topsn  21542  ordtbaslem  21799  ordtuni  21801  ordtbas2  21802  cnpco  21878  cnconst2  21894  tgcmp  22012  iunconn  22039  ptuni2  22187  xkococnlem  22270  tgqtop  22323  fbasrn  22495  uzrest  22508  fmco  22572  alexsubALT  22662  cnextf  22677  snclseqg  22727  ustund  22833  imasdsf1olem  22986  xmetresbl  23050  blsscls2  23117  metustss  23164  tngtopn  23262  reconn  23439  metnrmlem3  23472  cphsubrglem  23784  minveclem1  24030  minveclem3b  24034  ovolficcss  24073  ovolicc2lem4  24124  iundisj2  24153  uniioombllem4  24190  vitalilem5  24216  mbfeqalem1  24245  itg1addlem4  24303  limciun  24495  dvlip2  24595  dv11cn  24601  aalioulem3  24926  pserdvlem2  25019  pserdv  25020  abelthlem2  25023  efif1o  25133  efrlim  25550  lgamgulmlem1  25609  fsumdvdsmul  25775  perfectlem2  25809  setsvtx  26823  uhgredgn0  26916  upgredgss  26920  umgredgss  26921  usgredgss  26947  umgrres1lem  27095  upgrres1  27098  1hegrvtxdg1r  27293  clwlknf1oclwwlknlem3  27865  minvecolem1  28654  sh0le  29220  mdslmd3i  30112  iundisj2f  30343  suppss2f  30387  fnpreimac  30419  suppss3  30463  iundisj2fi  30523  lsmsnorb  30949  pstmfval  31140  ordtrest2NEW  31170  ldgenpisyslem1  31426  ldgenpisyslem2  31427  omsmeas  31585  sitgclbn  31605  eulerpartlemt  31633  eulerpartlemmf  31637  eulerpartlemgf  31641  bnj849  32201  bnj1136  32273  bnj1311  32300  bnj1413  32311  bnj1452  32328  blsconn  32495  cvmliftlem2  32537  cvmlift2lem12  32565  mvtss  32804  mthmpps  32833  trpredss  33072  trpredmintr  33074  noextendseq  33178  nosupno  33207  nosupbnd2lem1  33219  noetalem3  33223  neibastop2lem  33712  filnetlem3  33732  finxpsuclem  34682  poimirlem3  34899  mblfinlem3  34935  areacirclem2  34987  sdclem1  35022  istotbnd3  35053  sstotbnd  35057  iccbnd  35122  icccmpALT  35123  osumcllem1N  37096  osumcllem2N  37097  osumcllem4N  37099  osumcllem9N  37104  pexmidlem6N  37115  dihglblem3N  38435  dvhdimlem  38584  dochexmidlem6  38605  lcfrlem16  38698  lcfr  38725  hbtlem6  39735  iocinico  39824  trclubgNEW  39984  cnvrcl0  39991  relexp0a  40067  brtrclfv2  40078  cotrclrcl  40093  frege77d  40097  unhe1  40137  ntrrn  40478  imo72b2lem0  40522  imo72b2lem2  40524  imo72b2  40531  mnuprdlem4  40617  radcnvrat  40652  iunconnlem2  41275  ssinss2d  41328  limccog  41907  limsupresico  41987  liminfresico  42058  icccncfext  42176  stoweidlem14  42306  fourierdlem20  42419  fourierdlem42  42441  fourierdlem46  42444  fourierdlem50  42448  fourierdlem51  42449  fourierdlem54  42452  fourierdlem64  42462  fourierdlem76  42474  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  meadjiunlem  42754  meaiininclem  42775  ovnsupge0  42846  hoidmvlelem2  42885  hoidmvlelem4  42887  vonvolmbllem  42949  vonvolmbl2  42952  vonvol2  42953  vonioolem1  42969  issmflem  43011  fundcmpsurinjimaid  43578  perfectALTVlem2  43894  uspgropssxp  44026  funcrngcsetc  44276  funcringcsetc  44313  srhmsubc  44354  rhmsubclem3  44366  srhmsubcALTV  44372  rhmsubcALTVlem4  44385  setrec2fun  44802  onsetreclem2  44815
  Copyright terms: Public domain W3C validator