MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eqss Structured version   Unicode version

Theorem syl5eqss 3392
Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqss.1  |-  A  =  B
syl5eqss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5eqss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5eqss
StepHypRef Expression
1 syl5eqss.2 . 2  |-  ( ph  ->  B  C_  C )
2 syl5eqss.1 . . 3  |-  A  =  B
32sseq1i 3372 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3sylibr 204 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3320
This theorem is referenced by:  syl5eqssr  3393  inss  3570  tpssi  3965  fr3nr  4760  suceloni  4793  xpsspw  4986  xpsspwOLD  4987  fun  5607  fun11iun  5695  fmpt  5890  fliftrel  6030  knatar  6080  opabbrex  6118  suppss2  6300  1stcof  6374  2ndcof  6375  fnwelem  6461  oeeui  6845  cantnfp1lem1  7634  cantnfp1lem3  7636  cantnflem1d  7644  cantnflem1  7645  aceq3lem  8001  cflecard  8133  cfslb2n  8148  itunitc1  8300  axdc3lem2  8331  fpwwe2lem12  8516  canthwelem  8525  wuncval2  8622  gruiun  8674  peano5nni  10003  un0addcl  10253  un0mulcl  10254  mertenslem2  12662  4sqlem11  13323  4sqlem19  13331  vdwlem13  13361  imasless  13765  rescfth  14134  oppchofcl  14357  oyoncl  14367  gsumvallem1  14771  efgsfo  15371  efgcpbllemb  15387  frgpuplem  15404  gsumzaddlem  15526  dprdfid  15575  dprd2d2  15602  ablfacrp  15624  ablfac1b  15628  ablfac1eu  15631  pgpfac1lem5  15637  ablfaclem3  15645  lsptpcl  16055  lsppratlem3  16221  lsppratlem4  16222  lbsextlem2  16231  topsn  17000  ordtbaslem  17252  ordtuni  17254  ordtbas2  17255  cnpco  17331  cnconst2  17347  tgcmp  17464  iuncon  17491  ptuni2  17608  xkococnlem  17691  tgqtop  17744  fbasrn  17916  uzrest  17929  fmco  17993  alexsubALT  18082  cnextf  18097  snclseqg  18145  ustund  18251  imasdsf1olem  18403  xmetresbl  18467  blsscls2  18534  metustssOLD  18583  metustss  18584  tngtopn  18691  reconn  18859  metnrmlem3  18891  cphsubrglem  19140  minveclem1  19325  minveclem3b  19329  ovolficcss  19366  ovolicc2lem4  19416  iundisj2  19443  uniioombllem4  19478  vitalilem5  19504  mbfeqalem  19534  itg1addlem4  19591  limciun  19781  dvlip2  19879  dv11cn  19885  aalioulem3  20251  pserdvlem2  20344  pserdv  20345  abelthlem2  20348  efif1o  20448  efrlim  20808  fsumdvdsmul  20980  perfectlem2  21014  usgrares1  21424  eupares  21697  minvecolem1  22376  sh0le  22942  mdslmd3i  23835  iundisj2f  24030  suppss2f  24049  iundisj2fi  24153  pstmfval  24291  lgamgulmlem1  24813  blscon  24931  cvmliftlem2  24973  cvmlift2lem12  25001  ghomfo  25102  relexpdm  25135  relexprn  25136  trpredss  25507  trpredmintr  25509  frrlem5d  25589  mblfinlem3  26245  areacirclem2  26293  neibastop2lem  26389  filnetlem3  26409  sdclem1  26447  istotbnd3  26480  sstotbnd  26484  iccbnd  26549  icccmpALT  26550  f1lindf  27269  hbtlem6  27310  stoweidlem14  27739  iunconlem2  29047  bnj849  29296  bnj1136  29366  bnj1311  29393  bnj1413  29404  bnj1452  29421  osumcllem1N  30753  osumcllem2N  30754  osumcllem4N  30756  osumcllem9N  30761  pexmidlem6N  30772  dihglblem3N  32093  dvhdimlem  32242  dochexmidlem6  32263  lcfrlem16  32356  lcfr  32383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator