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

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

Proof of Theorem syl5eleqr
StepHypRef Expression
1 syl5eleqr.1 . 2 𝐴𝐵
2 syl5eleqr.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2812 . 2 (𝜑𝐵 = 𝐶)
41, 3syl5eleq 2891 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802
This theorem is referenced by:  rabsnt  4457  onnev  6061  opabiota  6482  canth  6832  onnseq  7677  tfrlem16  7725  oen0  7903  nnawordex  7954  inf0  8765  cantnflt  8816  cnfcom2  8846  cnfcom3lem  8847  cnfcom3  8848  r1ordg  8888  r1val1  8896  rankr1id  8972  acacni  9247  dfacacn  9248  dfac13  9249  cda1dif  9283  ttukeylem5  9620  ttukeylem6  9621  gch2  9782  gch3  9783  gchac  9788  gchina  9806  swrds1  13675  wrdl3s3  13930  sadcp1  15396  lcmfunsnlem2  15572  xpsfrnel2  16430  idfucl  16745  gsumval2  17485  gsumz  17579  frmdmnd  17601  frmd0  17602  efginvrel2  18341  efgcpbl2  18371  pgpfaclem1  18682  lbsexg  19373  zringndrg  20046  frlmlbs  20346  mat0dimscm  20486  mat0scmat  20555  m2detleiblem5  20642  m2detleiblem6  20643  m2detleiblem3  20646  m2detleiblem4  20647  d0mat2pmat  20756  chpmat0d  20852  dfac14  21635  acufl  21934  cnextfvval  22082  cnextcn  22084  minveclem3b  23411  minveclem4a  23413  ovollb2  23470  ovolunlem1a  23477  ovolunlem1  23478  ovoliunlem1  23483  ovoliun2  23487  ioombl1lem4  23542  uniioombllem1  23562  uniioombllem2  23564  uniioombllem6  23569  itg2monolem1  23731  itg2mono  23734  itg2cnlem1  23742  xrlimcnp  24909  efrlim  24910  eengbas  26075  ebtwntg  26076  ecgrtg  26077  elntg  26078  wlkl1loop  26762  elwwlks2ons3im  27094  elwwlks2ons3OLD  27096  upgr3v3e3cycl  27353  upgr4cycl4dv4e  27358  2clwwlk2clwwlk  27527  ex-br  27619  rge0scvg  30320  repr0  31014  hgt750lemg  31057  mrsub0  31736  elmrsubrn  31740  topjoin  32681  pclfinN  35680  aomclem1  38125  dfac21  38137  clsk1indlem1  38843  fourierdlem102  40904  fourierdlem114  40916  lincval0  42772  lcoel0  42785
  Copyright terms: Public domain W3C validator