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

Theorem syl6eqel 2738
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 2730 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  syl6eqelr  2739  csbexg  4825  unisn2  4827  class2set  4862  snexALT  4882  snex  4938  prex  4939  onun2i  5881  iotaex  5906  fvrn0  6254  f0cli  6410  funsneqop  6458  fmptsng  6475  fmptsnd  6476  elimdelov  6778  ovima0  6855  ndmovcl  6861  caovmo  6913  soex  7151  zfrep6  7176  1st2ndb  7250  wfrlem17  7476  smofvon2  7498  tz7.44-2  7548  oesuclem  7650  omcl  7661  oecl  7662  nnmcl  7737  nnecl  7738  ixpexg  7974  resixpfo  7988  en1b  8065  xpsnen  8085  nnunifi  8252  xpfi  8272  fsuppun  8335  0fsupp  8338  oiexg  8481  hartogslem1  8488  cantnfvalf  8600  rankdmr1  8702  rankr1c  8722  numwdom  8920  alephon  8930  isfin5  9159  sdom2en01  9162  isf32lem9  9221  hsmexlem9  9285  iundom2g  9400  gchxpidm  9529  r1tskina  9642  tskmcl  9701  recmulnq  9824  recclnq  9826  genpelv  9860  un0mulcl  11365  znegcl  11450  zeo  11501  eqreznegel  11812  xnegcl  12082  xnn0xaddcl  12104  ioorebas  12313  modid0  12736  2txmodxeq0  12770  fzofi  12813  expcllem  12911  m1expcl2  12922  faclbnd4lem3  13122  bccl  13149  hasheq0  13192  hashrabrsn  13199  fnfz0hashnn0  13270  fnfzo0hashnn0  13273  ccat2s1p1  13449  cshwcl  13590  relexpaddg  13837  abs00bd  14075  iserge0  14435  sumrblem  14486  fsumcvg  14487  summolem2a  14490  sumss  14499  fsumss  14500  fsumcvg2  14502  sumsplit  14543  binom  14606  bcxmas  14611  geomulcvg  14651  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  zprod  14711  fprodntriv  14716  prodss  14721  fprodss  14722  binomfallfac  14816  bpoly1  14826  bpoly2  14832  bpoly3  14833  ruclem6  15008  smupf  15247  gcdcl  15275  lcmcl  15361  lcmfcl  15388  pcxcl  15612  pcmptcl  15642  infpnlem2  15662  zgz  15684  4sqlem2  15700  4sqlem19  15714  vdwapval  15724  hashbc0  15756  ramcl2  15767  0ramcl  15774  ramcl  15780  isstruct2  15914  imasval  16218  imasbas  16219  imasds  16220  imasplusg  16224  imasmulr  16225  imasvsca  16227  imasip  16228  imasle  16230  qusaddvallem  16258  qusaddflem  16259  qusaddval  16260  qusaddf  16261  qusmulval  16262  qusmulf  16263  mreexexlem3d  16353  sscpwex  16522  fullresc  16558  estrres  16826  evlfcl  16909  ipopos  17207  gsumress  17323  submnd0  17367  qusgrp2  17580  issubg2  17656  torsubg  18303  frgpnabllem1  18322  lt6abl  18342  ablfaclem3  18532  ablfac2  18534  srgbinomlem3  18588  ringidss  18623  qusring2  18666  isdrngd  18820  mptscmfsupp0  18976  islss3  19007  lspsnel  19051  lspprel  19142  znf1o  19948  frgpcyg  19970  cnmsgnsubg  19971  phlpropd  20048  cssval  20074  iscss  20075  dsmm0cl  20132  uvcvvcl  20174  m1detdiag  20451  m2detleiblem1  20478  pmatcollpw3fi1lem1  20639  indistopon  20853  indiscld  20943  restbas  21010  ordttopon  21045  iocpnfordt  21067  icomnfordt  21068  lecldbas  21071  fiuncmp  21255  cmpfi  21259  conncompid  21282  dissnlocfin  21380  elpt  21423  xkotop  21439  xkouni  21450  xkohaus  21504  xkoptsub  21505  imastopn  21571  filconn  21734  cfinufil  21779  alexsublem  21895  alexsub  21896  alexsubALTlem4  21901  distgp  21950  indistgp  21951  ssblps  22274  ssbl  22275  xmeter  22285  nmoi  22579  nmoeq0  22587  0nghm  22592  idnghm  22594  icccld  22617  iocmnfcld  22619  blssioo  22645  xrtgioo  22656  xrsxmet  22659  icccmp  22675  pcopt  22868  pcopt2  22869  elpi1  22891  cmetcaulem  23132  ishl2  23212  rrxmvallem  23233  ovolcl  23292  ovolunlem1a  23310  ovolunnul  23314  ovoliunnul  23321  ioombl1  23376  icombl  23378  ioombl  23379  iccmbl  23380  iccvolcl  23381  ovolioo  23382  ioovolcl  23384  ioorcl  23391  uniioovol  23393  uniioombllem2a  23396  uniioombllem4  23400  uniioombllem5  23401  vitalilem1  23422  vitalilem5  23426  mbfconstlem  23441  mbfima  23444  mbfid  23448  ismbf2d  23453  mbfss  23458  mbfmulc2lem  23459  i1fd  23493  itg1addlem2  23509  itg1addlem4  23511  itg1addlem5  23512  i1fmulc  23515  itg2l  23541  itg2cl  23544  ibl0  23598  iblrelem  23602  iblpos  23604  iblss2  23617  bddmulibl  23650  recnperf  23714  ply1remlem  23967  fta1glem1  23970  fta1g  23972  elply  23996  plypf1  24013  coefv0  24049  coemulc  24056  fta1  24108  elqaalem2  24120  aannenlem2  24129  aalioulem3  24134  taylfvallem1  24156  tayl0  24161  ulm0  24190  logtayl  24451  atanrecl  24683  atanbnd  24698  harmonicbnd3  24779  ftalem7  24850  basellem5  24856  ppifi  24877  sqff1o  24953  1sgmprm  24969  logexprlim  24995  dchrelbasd  25009  dchr1re  25033  lgslem4  25070  lgsne0  25105  2sqlem9  25197  2sqlem10  25198  rpvmasumlem  25221  dchrisumlem1  25223  vmalogdivsum  25273  pntrlog2bndlem5  25315  ostth  25373  tgcgr4  25471  axlowdimlem16  25882  fusgrfisbase  26265  vtxdg0e  26426  rgrusgrprc  26541  clwwlknfi  27008  trlsegvdeglem7  27204  eulerpathpr  27218  0blo  27775  nmlno0lem  27776  omlsilem  28389  pjoc1i  28418  nonbooli  28638  nmlnop0iALT  28982  unopbd  29002  leoprf2  29114  opsqrlem4  29130  opsqrlem5  29131  pjbdlni  29136  pjcmul1i  29188  prsssdm  30091  ordtrestNEW  30095  esumpad  30245  esumpad2  30246  esumcst  30253  esumrnmpt2  30258  sibf0  30524  sitgclcn  30534  sitgclre  30535  eulerpartlemgs2  30570  dstfrvclim1  30667  ballotlemfelz  30680  sgncl  30728  signstfveq0  30782  breprexp  30839  subfacp1lem3  31290  rellysconn  31359  cvmlift2lem9  31419  ordcmp  32571  finxpreclem4  33361  poimirlem16  33555  poimirlem17  33556  voliunnfl  33583  mbfresfi  33586  itg2addnclem2  33592  bddiblnc  33610  dvasin  33626  heiborlem4  33743  heiborlem6  33745  wepwsolem  37929  flcidc  38061  iocmbl  38115  arearect  38118  briunov2uz  38307  eliunov2uz  38308  frege124d  38370  frege129d  38372  frege92  38566  lhe4.4ex1a  38845  dvconstbi  38850  binomcxplemnn0  38865  binomcxplemnotnn0  38872  infxr  39896  infleinflem2  39900  climneg  40160  cncfiooicc  40425  itgsinexplem1  40487  volioof  40522  stoweidlem36  40571  wallispilem3  40602  fourierdlem93  40734  fouriersw  40766  fouriercn  40767  etransclem16  40785  etransclem33  40802  sge0reuz  40982  nnfoctbdjlem  40990  hoidmvlelem3  41132  fmtnofz04prm  41814  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  sprsymrelfvlem  42065  lincext2  42569  blennn0elnn  42696
  Copyright terms: Public domain W3C validator