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

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

Proof of Theorem syl5eqelr
StepHypRef Expression
1 syl5eqelr.1 . . 3 𝐵 = 𝐴
21eqcomi 2774 . 2 𝐴 = 𝐵
3 syl5eqelr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqel 2848 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-clel 2761
This theorem is referenced by:  3eltr3g  2860  dmrnssfld  5553  oprssdm  7013  offval  7102  pwexr  7172  cnvexg  7310  resfunexgALT  7327  abrexexg  7338  abrexex2g  7342  opabex3d  7343  suppssov1  7530  suppssfv  7534  ralxpmap  8112  residfi  8454  imafi  8466  abrexfi  8473  ssfii  8532  wdomima2g  8698  unxpwdom2  8700  tskwe  9027  ac10ct  9108  fin23lem28  9415  fin23lem30  9417  axcclem  9532  distrlem4pr  10101  iccshftr  12513  iccshftl  12515  iccdil  12517  icccntr  12519  o1res  14578  exprmfct  15697  infpnlem1  15895  4sqlem13  15942  0ram  16005  ressval3d  16211  ressval3dOLD  16212  ismred2  16531  mreexexlem2d  16573  mreexexlem4d  16575  acsfn1c  16590  acsfn2  16591  ssclem  16746  submacs  17633  efgrcl  18394  dprd2da  18708  srgbinom  18812  irredlmul  18975  lidlrsppropd  19504  issubassa  19598  ply1crng  19841  ply1ring  19891  ply1lmod  19895  chrcl  20147  css1  20310  oftpos  20535  tposmap  20540  0opn  20988  fctop2  21089  difopn  21118  tgrest  21243  ordtbas2  21275  ordtopn3  21280  ordtcld3  21283  t1ficld  21411  resthauslem  21447  kgentopon  21621  txbasex  21649  txcnpi  21691  txdis1cn  21718  pthaus  21721  txkgen  21735  cnmptid  21744  cnmptc  21745  cnmpt1st  21751  cnmpt2nd  21752  cnmpt2c  21753  cnmptkc  21762  txconn  21772  hmeoima  21848  hmeocld  21850  xkohmeo  21898  filufint  22003  fin1aufil  22015  flftg  22079  ptcmplem2  22136  tmdmulg  22175  tmdgsum2  22179  symgtgp  22184  submtmd  22187  ghmcnp  22197  qustgpopn  22202  qustgplem  22203  ust0  22302  nrginvrcn  22775  fsumcn  22952  fsum2cn  22953  expcn  22954  cnheibor  23033  evth2  23038  csscld  23326  clsocv  23327  ovoliun2  23564  volfiniun  23605  dyadmbl  23658  mbfeqalem2  23700  mbfss  23704  ismbf3d  23712  mbfadd  23719  i1f0rn  23740  mbfmul  23784  itg2seq  23800  itg2monolem2  23809  itg2monolem3  23810  itg2mono  23811  itgreval  23854  itgge0  23868  itgss3  23872  iblconst  23875  itgconst  23876  ibladdlem  23877  itgfsum  23884  iblabslem  23885  itgabs  23892  mvth  24046  lhop1lem  24067  dvfsumle  24075  dvfsumlem2  24081  ftc1lem4  24093  itgparts  24101  itgsubstlem  24102  itgsubst  24103  plydivlem1  24339  aannenlem1  24374  taylply2  24413  itgulm  24453  cxpcn  24777  resqrtcn  24781  basellem1  25098  mulogsumlem  25511  mulog2sumlem2  25515  selberg2lem  25530  pntrsumo1  25545  usgrnbcnvfv  26545  ewlksfval  26788  crctcshwlkn0  27005  numclwwlk3lemOLD  27632  pjssmii  28931  abrexexd  29731  ogrpaddltrbid  30103  lmatfval  30262  pl1cn  30383  esumcvg  30530  esumcvgsum  30532  sigaval  30555  sigaclfu2  30566  sigapildsys  30607  ldgenpisys  30611  measinb2  30668  braew  30687  unelcarsg  30756  carsgclctunlem2  30763  sibfof  30784  sitgclg  30786  orrvcoel  30910  orrvccel  30911  fsum2dsub  31068  subfaclefac  31538  cvmsss2  31636  cvmopnlem  31640  mpstrcl  31818  elmpps  31850  hmeoclda  32703  bj-1uplex  33355  bj-2uplex  33369  bj-diagval  33456  icoreclin  33570  cnfinltrel  33606  broucube  33799  mblfinlem1  33802  cnambfre  33813  ibladdnclem  33821  iblabsnclem  33828  itgabsnc  33834  ftc1cnnclem  33838  ftc1anclem4  33843  ftc1anclem5  33844  ftc1anclem6  33845  ftc1anclem7  33846  ftc2nc  33849  areacirc  33860  zrdivrng  34106  xrnresex  34525  dalemrot  35545  dalem10  35561  arglem1N  36078  cdlemk36  36801  mzpconstmpt  37913  mzpresrename  37923  diophrex  37949  0dioph  37952  anrabdioph  37954  orrabdioph  37955  rabren3dioph  37989  iunrelexp0  38601  dvradcnv2  39152  xpexb  39262  fsumcnf  39764  uzublem  40226  fprodcncf  40684  iblconstmpt  40741  itgiccshift  40765  itgperiod  40766  itgsbtaddcnst  40767  dirkercncflem2  40890  fourierdlem47  40939  saluni  41113  sge0iunmpt  41204  sge0xaddlem2  41220  sge0xadd  41221  hoidmvlelem3  41383  ctvonmbl  41475  vonct  41479  smfaddlem2  41544  smfmullem4  41573  aoprssdm  41882
  Copyright terms: Public domain W3C validator