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

Theorem syl6eqel 2918
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 2910 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  syl6eqelr  2919  csbexg  5205  unisn2  5207  class2set  5245  snexALT  5274  snex  5322  prex  5323  onun2i  6299  iotaex  6328  fvrn0  6691  f0cli  6856  funsneqopb  6906  fmptsng  6922  fmptsnd  6923  elimdelov  7239  ovima0  7316  ndmovcl  7322  caovmo  7374  soex  7615  zfrep6  7645  1st2ndb  7718  wfrlem17  7960  smofvon2  7982  tz7.44-2  8032  oesuclem  8139  omcl  8150  oecl  8151  nnmcl  8227  nnecl  8228  ixpexg  8474  resixpfo  8488  en1b  8565  xpsnen  8589  nnunifi  8757  xpfi  8777  fsuppun  8840  0fsupp  8843  oiexg  8987  hartogslem1  8994  cantnfvalf  9116  rankdmr1  9218  rankr1c  9238  numwdom  9473  alephon  9483  isfin5  9709  sdom2en01  9712  isf32lem9  9771  hsmexlem9  9835  iundom2g  9950  gchxpidm  10079  r1tskina  10192  tskmcl  10251  recmulnq  10374  recclnq  10376  genpelv  10410  un0mulcl  11919  znegcl  12005  zeo  12056  eqreznegel  12322  xnegcl  12594  xnn0xaddcl  12616  ioorebas  12827  modid0  13253  2txmodxeq0  13287  fzofi  13330  seqexw  13373  expcllem  13428  m1expcl2  13439  faclbnd4lem3  13643  bccl  13670  hasheq0  13712  hashrabrsn  13721  fnfz0hashnn0  13794  fnfzo0hashnn0  13797  wrdnfi  13887  ccat2s1p1OLD  13975  cshwcl  14148  relexpaddg  14400  abs00bd  14639  iserge0  15005  sumrblem  15056  fsumcvg  15057  summolem2a  15060  sumss  15069  fsumss  15070  fsumcvg2  15072  sumsplit  15111  binom  15173  bcxmas  15178  geomulcvg  15220  prodrblem  15271  fprodcvg  15272  prodmolem2a  15276  zprod  15279  fprodntriv  15284  prodss  15289  fprodss  15290  binomfallfac  15383  bpoly1  15393  bpoly2  15399  bpoly3  15400  ruclem6  15576  smupf  15815  gcdcl  15843  lcmcl  15933  lcmfcl  15960  2mulprm  16025  pcxcl  16185  pcmptcl  16215  infpnlem2  16235  zgz  16257  4sqlem2  16273  4sqlem19  16287  vdwapval  16297  hashbc0  16329  ramcl2  16340  0ramcl  16347  ramcl  16353  isstruct2  16481  imasval  16772  imasbas  16773  imasds  16774  imasplusg  16778  imasmulr  16779  imasvsca  16781  imasip  16782  imasle  16784  qusaddvallem  16812  qusaddflem  16813  qusaddval  16814  qusaddf  16815  qusmulval  16816  qusmulf  16817  mreexexlem3d  16905  sscpwex  17073  fullresc  17109  estrres  17377  evlfcl  17460  ipopos  17758  gsumress  17880  submnd0  17928  qusgrp2  18155  mulgfval  18164  issubg2  18232  triv1nsgd  18263  torsubg  18903  frgpnabllem1  18922  lt6abl  18944  ablfaclem3  19138  ablfac2  19140  simpgnsgd  19151  srgbinomlem3  19221  ringidss  19256  qusring2  19299  isdrngd  19456  mptscmfsupp0  19628  islss3  19660  lspsnel  19704  lspprel  19795  znf1o  20626  frgpcyg  20648  cnmsgnsubg  20649  phlpropd  20727  cssval  20754  iscss  20755  dsmm0cl  20812  uvcvvcl  20859  m1detdiag  21134  m2detleiblem1  21161  pmatcollpw3fi1lem1  21322  indistopon  21537  indiscld  21627  restbas  21694  ordttopon  21729  iocpnfordt  21751  icomnfordt  21752  lecldbas  21755  fiuncmp  21940  cmpfi  21944  conncompid  21967  dissnlocfin  22065  elpt  22108  xkotop  22124  xkouni  22135  xkohaus  22189  xkoptsub  22190  imastopn  22256  filconn  22419  cfinufil  22464  alexsublem  22580  alexsub  22581  alexsubALTlem4  22586  distgp  22635  indistgp  22636  ssblps  22959  ssbl  22960  xmeter  22970  nmoi  23264  nmoeq0  23272  0nghm  23277  idnghm  23279  icccld  23302  iocmnfcld  23304  blssioo  23330  xrtgioo  23341  xrsxmet  23344  icccmp  23360  pcopt  23553  pcopt2  23554  elpi1  23576  cmetcaulem  23818  ishl2  23900  rrxmvallem  23934  ovolcl  24006  ovolunlem1a  24024  ovolunnul  24028  ovoliunnul  24035  ioombl1  24090  icombl  24092  ioombl  24093  iccmbl  24094  iccvolcl  24095  ovolioo  24096  ioovolcl  24098  ioorcl  24105  uniioovol  24107  uniioombllem2a  24110  uniioombllem4  24114  uniioombllem5  24115  vitalilem1  24136  vitalilem5  24140  mbfconstlem  24155  mbfima  24158  mbfid  24163  ismbf2d  24168  mbfss  24174  mbfmulc2lem  24175  i1fd  24209  itg1addlem2  24225  itg1addlem4  24227  itg1addlem5  24228  i1fmulc  24231  itg2l  24257  itg2cl  24260  ibl0  24314  iblrelem  24318  iblpos  24320  iblss2  24333  bddmulibl  24366  recnperf  24430  ply1remlem  24683  fta1glem1  24686  fta1g  24688  elply  24712  plypf1  24729  coefv0  24765  coemulc  24772  fta1  24824  elqaalem2  24836  aannenlem2  24845  aalioulem3  24850  taylfvallem1  24872  tayl0  24877  ulm0  24906  logtayl  25170  atanrecl  25416  atanbnd  25431  harmonicbnd3  25512  ftalem7  25583  basellem5  25589  ppifi  25610  sqff1o  25686  1sgmprm  25702  logexprlim  25728  dchrelbasd  25742  dchr1re  25766  lgslem4  25803  lgsne0  25838  2sqlem9  25930  2sqlem10  25931  rpvmasumlem  25990  dchrisumlem1  25992  vmalogdivsum  26042  pntrlog2bndlem5  26084  ostth  26142  tgcgr4  26244  axlowdimlem16  26670  fusgrfisbase  27037  vtxdg0e  27183  rgrusgrprc  27298  wwlksnfi  27611  clwwlknfiOLD  27751  trlsegvdeglem7  27932  eulerpathpr  27946  0blo  28496  nmlno0lem  28497  omlsilem  29106  pjoc1i  29135  nonbooli  29355  nmlnop0iALT  29699  unopbd  29719  leoprf2  29831  opsqrlem4  29847  opsqrlem5  29848  pjbdlni  29853  pjcmul1i  29905  prsssdm  31059  ordtrestNEW  31063  esumpad  31213  esumpad2  31214  esumcst  31221  esumrnmpt2  31226  sibf0  31491  sitgclcn  31501  sitgclre  31502  eulerpartlemgs2  31537  dstfrvclim1  31634  ballotlemfelz  31647  sgncl  31695  signstfveq0  31746  breprexp  31803  subfacp1lem3  32326  rellysconn  32395  cvmlift2lem9  32455  ordcmp  33692  finxpreclem4  34557  poimirlem16  34789  poimirlem17  34790  voliunnfl  34817  mbfresfi  34819  itg2addnclem2  34825  bddiblnc  34843  dvasin  34859  heiborlem4  34973  heiborlem6  34975  wepwsolem  39520  flcidc  39652  iocmbl  39697  arearect  39700  iscard4  39778  briunov2uz  39921  eliunov2uz  39922  frege124d  39984  frege129d  39986  frege92  40179  lhe4.4ex1a  40538  dvconstbi  40543  binomcxplemnn0  40558  binomcxplemnotnn0  40565  infxr  41511  infleinflem2  41515  climneg  41767  cncfiooicc  42053  itgsinexplem1  42115  volioof  42149  stoweidlem36  42198  wallispilem3  42229  fourierdlem93  42361  fouriersw  42393  fouriercn  42394  etransclem16  42412  etransclem33  42429  sge0reuz  42606  nnfoctbdjlem  42614  hoidmvlelem3  42756  dfatafv2ex  43289  sprsymrelfvlem  43529  fmtnofz04prm  43616  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  lincext2  44438  blennn0elnn  44565
  Copyright terms: Public domain W3C validator