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

Theorem syl6eqel 2919
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqel.1 (𝜑𝐴 = 𝐵)
syl6eqel.2 𝐵𝐶
Assertion
Ref Expression
syl6eqel (𝜑𝐴𝐶)

Proof of Theorem syl6eqel
StepHypRef Expression
1 syl6eqel.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqel.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqeltrd 2911 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-clel 2891
This theorem is referenced by:  eqeltrrdi  2920  csbexg  5205  unisn2  5207  class2set  5245  snexALT  5274  snex  5322  prex  5323  onun2i  6299  iotaex  6328  fvrn0  6691  f0cli  6857  funsneqopb  6907  fmptsng  6923  fmptsnd  6924  elimdelov  7242  ovima0  7319  ndmovcl  7325  caovmo  7377  soex  7618  zfrep6  7648  1st2ndb  7721  wfrlem17  7963  smofvon2  7985  tz7.44-2  8035  oesuclem  8142  omcl  8153  oecl  8154  nnmcl  8230  nnecl  8231  ixpexg  8478  resixpfo  8492  en1b  8569  xpsnen  8593  nnunifi  8761  xpfi  8781  fsuppun  8844  0fsupp  8847  oiexg  8991  hartogslem1  8998  cantnfvalf  9120  rankdmr1  9222  rankr1c  9242  numwdom  9477  alephon  9487  isfin5  9713  sdom2en01  9716  isf32lem9  9775  hsmexlem9  9839  iundom2g  9954  gchxpidm  10083  r1tskina  10196  tskmcl  10255  recmulnq  10378  recclnq  10380  genpelv  10414  un0mulcl  11923  znegcl  12009  zeo  12060  eqreznegel  12326  xnegcl  12598  xnn0xaddcl  12620  ioorebas  12831  modid0  13257  2txmodxeq0  13291  fzofi  13334  seqexw  13377  expcllem  13432  m1expcl2  13443  faclbnd4lem3  13647  bccl  13674  hasheq0  13716  hashrabrsn  13725  fnfz0hashnn0  13798  fnfzo0hashnn0  13801  wrdnfi  13891  ccat2s1p1OLD  13979  cshwcl  14152  relexpaddg  14404  abs00bd  14643  iserge0  15009  sumrblem  15060  fsumcvg  15061  summolem2a  15064  sumss  15073  fsumss  15074  fsumcvg2  15076  sumsplit  15115  binom  15177  bcxmas  15182  geomulcvg  15224  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  fprodntriv  15288  prodss  15293  fprodss  15294  binomfallfac  15387  bpoly1  15397  bpoly2  15403  bpoly3  15404  ruclem6  15580  smupf  15819  gcdcl  15847  lcmcl  15937  lcmfcl  15964  2mulprm  16029  pcxcl  16189  pcmptcl  16219  infpnlem2  16239  zgz  16261  4sqlem2  16277  4sqlem19  16291  vdwapval  16301  hashbc0  16333  ramcl2  16344  0ramcl  16351  ramcl  16357  isstruct2  16485  imasval  16776  imasbas  16777  imasds  16778  imasplusg  16782  imasmulr  16783  imasvsca  16785  imasip  16786  imasle  16788  qusaddvallem  16816  qusaddflem  16817  qusaddval  16818  qusaddf  16819  qusmulval  16820  qusmulf  16821  mreexexlem3d  16909  sscpwex  17077  fullresc  17113  estrres  17381  evlfcl  17464  ipopos  17762  gsumress  17884  submnd0  17932  qusgrp2  18209  mulgfval  18218  issubg2  18286  triv1nsgd  18317  torsubg  18966  frgpnabllem1  18985  lt6abl  19007  ablfaclem3  19201  ablfac2  19203  simpgnsgd  19214  srgbinomlem3  19284  ringidss  19319  qusring2  19362  isdrngd  19519  mptscmfsupp0  19691  islss3  19723  lspsnel  19767  lspprel  19858  znf1o  20690  frgpcyg  20712  cnmsgnsubg  20713  phlpropd  20791  cssval  20818  iscss  20819  dsmm0cl  20876  uvcvvcl  20923  m1detdiag  21198  m2detleiblem1  21225  pmatcollpw3fi1lem1  21386  indistopon  21601  indiscld  21691  restbas  21758  ordttopon  21793  iocpnfordt  21815  icomnfordt  21816  lecldbas  21819  fiuncmp  22004  cmpfi  22008  conncompid  22031  dissnlocfin  22129  elpt  22172  xkotop  22188  xkouni  22199  xkohaus  22253  xkoptsub  22254  imastopn  22320  filconn  22483  cfinufil  22528  alexsublem  22644  alexsub  22645  alexsubALTlem4  22650  distgp  22699  indistgp  22700  ssblps  23024  ssbl  23025  xmeter  23035  nmoi  23329  nmoeq0  23337  0nghm  23342  idnghm  23344  icccld  23367  iocmnfcld  23369  blssioo  23395  xrtgioo  23406  xrsxmet  23409  icccmp  23425  pcopt  23618  pcopt2  23619  elpi1  23641  cmetcaulem  23883  ishl2  23965  rrxmvallem  23999  ovolcl  24071  ovolunlem1a  24089  ovolunnul  24093  ovoliunnul  24100  ioombl1  24155  icombl  24157  ioombl  24158  iccmbl  24159  iccvolcl  24160  ovolioo  24161  ioovolcl  24163  ioorcl  24170  uniioovol  24172  uniioombllem2a  24175  uniioombllem4  24179  uniioombllem5  24180  vitalilem1  24201  vitalilem5  24205  mbfconstlem  24220  mbfima  24223  mbfid  24228  ismbf2d  24233  mbfss  24239  mbfmulc2lem  24240  i1fd  24274  itg1addlem2  24290  itg1addlem4  24292  itg1addlem5  24293  i1fmulc  24296  itg2l  24322  itg2cl  24325  ibl0  24379  iblrelem  24383  iblpos  24385  iblss2  24398  bddmulibl  24431  recnperf  24495  ply1remlem  24748  fta1glem1  24751  fta1g  24753  elply  24777  plypf1  24794  coefv0  24830  coemulc  24837  fta1  24889  elqaalem2  24901  aannenlem2  24910  aalioulem3  24915  taylfvallem1  24937  tayl0  24942  ulm0  24971  logtayl  25235  atanrecl  25481  atanbnd  25496  harmonicbnd3  25577  ftalem7  25648  basellem5  25654  ppifi  25675  sqff1o  25751  1sgmprm  25767  logexprlim  25793  dchrelbasd  25807  dchr1re  25831  lgslem4  25868  lgsne0  25903  2sqlem9  25995  2sqlem10  25996  rpvmasumlem  26055  dchrisumlem1  26057  vmalogdivsum  26107  pntrlog2bndlem5  26149  ostth  26207  tgcgr4  26309  axlowdimlem16  26735  fusgrfisbase  27102  vtxdg0e  27248  rgrusgrprc  27363  wwlksnfi  27676  clwwlknfiOLD  27816  trlsegvdeglem7  27997  eulerpathpr  28011  0blo  28561  nmlno0lem  28562  omlsilem  29171  pjoc1i  29200  nonbooli  29420  nmlnop0iALT  29764  unopbd  29784  leoprf2  29896  opsqrlem4  29912  opsqrlem5  29913  pjbdlni  29918  pjcmul1i  29970  prsssdm  31148  ordtrestNEW  31152  esumpad  31302  esumpad2  31303  esumcst  31310  esumrnmpt2  31315  sibf0  31580  sitgclcn  31590  sitgclre  31591  eulerpartlemgs2  31626  dstfrvclim1  31723  ballotlemfelz  31736  sgncl  31784  signstfveq0  31835  breprexp  31892  subfacp1lem3  32417  rellysconn  32486  cvmlift2lem9  32546  ordcmp  33783  bj-indiscrmoore  34393  finxpreclem4  34657  poimirlem16  34890  poimirlem17  34891  voliunnfl  34918  mbfresfi  34920  itg2addnclem2  34926  bddiblnc  34944  dvasin  34960  heiborlem4  35074  heiborlem6  35076  wepwsolem  39622  flcidc  39754  iocmbl  39799  arearect  39802  iscard4  39880  briunov2uz  40023  eliunov2uz  40024  frege124d  40086  frege129d  40088  frege92  40281  lhe4.4ex1a  40641  dvconstbi  40646  binomcxplemnn0  40661  binomcxplemnotnn0  40668  infxr  41614  infleinflem2  41618  climneg  41870  cncfiooicc  42156  itgsinexplem1  42218  volioof  42252  stoweidlem36  42301  wallispilem3  42332  fourierdlem93  42464  fouriersw  42496  fouriercn  42497  etransclem16  42515  etransclem33  42532  sge0reuz  42709  nnfoctbdjlem  42717  hoidmvlelem3  42859  dfatafv2ex  43392  sprsymrelfvlem  43632  fmtnofz04prm  43719  nnsum4primeseven  43945  nnsum4primesevenALTV  43946  lincext2  44490  blennn0elnn  44617
  Copyright terms: Public domain W3C validator