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

Theorem syl5eqelr 2693
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 2619 . 2 𝐴 = 𝐵
3 syl5eqelr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqel 2692 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  3eltr3g  2704  dmrnssfld  5292  oprssdm  6691  offval  6780  cnvexg  6983  resfunexgALT  7000  abrexexg  7012  abrexex2g  7014  opabex3d  7015  suppssov1  7192  suppssfv  7196  ralxpmap  7771  imafi  8120  abrexfi  8127  ssfii  8186  wdomima2g  8352  unxpwdom2  8354  tskwe  8637  ac10ct  8718  fin23lem28  9023  fin23lem30  9025  axcclem  9140  distrlem4pr  9705  iccshftr  12136  iccshftl  12138  iccdil  12140  icccntr  12142  o1res  14088  exprmfct  15203  infpnlem1  15401  4sqlem13  15448  0ram  15511  ressval3d  15713  ismred2  16035  mreexexlem2d  16077  mreexexlem4d  16079  acsfn1c  16095  acsfn2  16096  ssclem  16251  submacs  17137  efgrcl  17900  dprd2da  18213  srgbinom  18317  irredlmul  18480  lidlrsppropd  19000  issubassa  19094  ply1crng  19338  ply1ring  19388  ply1lmod  19392  chrcl  19641  css1  19801  oftpos  20025  tposmap  20030  0opn  20482  fctop2  20567  difopn  20596  tgrest  20721  ordtbas2  20753  ordtopn3  20758  ordtcld3  20761  t1ficld  20889  resthauslem  20925  kgentopon  21099  txbasex  21127  txcnpi  21169  txdis1cn  21196  pthaus  21199  txkgen  21213  cnmptid  21222  cnmptc  21223  cnmpt1st  21229  cnmpt2nd  21230  cnmpt2c  21231  cnmptkc  21240  txcon  21250  hmeoima  21326  hmeocld  21328  xkohmeo  21376  filufint  21482  fin1aufil  21494  flftg  21558  ptcmplem2  21615  tmdmulg  21654  tmdgsum2  21658  symgtgp  21663  submtmd  21666  ghmcnp  21676  qustgpopn  21681  qustgplem  21682  ust0  21781  nrginvrcn  22254  fsumcn  22429  fsum2cn  22430  expcn  22431  cnheibor  22510  evth2  22515  csscld  22801  clsocv  22802  ovoliun2  23026  volfiniun  23067  dyadmbl  23119  mbfeqalem  23160  mbfss  23164  ismbf3d  23172  mbfadd  23179  i1f0rn  23200  mbfmul  23244  itg2seq  23260  itg2monolem2  23269  itg2monolem3  23270  itg2mono  23271  itgreval  23314  itgge0  23328  itgss3  23332  iblconst  23335  itgconst  23336  ibladdlem  23337  itgfsum  23344  iblabslem  23345  itgabs  23352  mvth  23504  lhop1lem  23525  dvfsumle  23533  dvfsumlem2  23539  ftc1lem4  23551  itgparts  23559  itgsubstlem  23560  itgsubst  23561  plydivlem1  23797  aannenlem1  23832  taylply2  23871  itgulm  23911  cxpcn  24231  resqrtcn  24235  basellem1  24552  mulogsumlem  24965  mulog2sumlem2  24969  selberg2lem  24984  pntrsumo1  24999  nbgracnvfv  25763  pjssmii  27718  abrexexd  28525  ogrpaddltrbid  28846  lmatfval  29002  pl1cn  29123  esumcvg  29269  esumcvgsum  29271  sigaval  29294  sigaclfu2  29305  sigapildsys  29346  ldgenpisys  29350  measinb2  29407  braew  29426  unelcarsg  29495  carsgclctunlem2  29502  sibfof  29523  sitgclg  29525  orrvcoel  29648  orrvccel  29649  subfaclefac  30206  cvmsss2  30304  cvmopnlem  30308  mpstrcl  30486  elmpps  30518  hmeoclda  31292  bj-1uplex  31983  bj-2uplex  31997  bj-diagval  32061  icoreclin  32175  broucube  32407  mblfinlem1  32410  cnambfre  32422  ibladdnclem  32430  iblabsnclem  32437  itgabsnc  32443  ftc1cnnclem  32447  ftc1anclem4  32452  ftc1anclem5  32453  ftc1anclem6  32454  ftc1anclem7  32455  ftc2nc  32458  areacirc  32469  zrdivrng  32716  dalemrot  33755  dalem10  33771  arglem1N  34289  cdlemk36  35013  mzpconstmpt  36115  mzpresrename  36125  diophrex  36151  0dioph  36154  anrabdioph  36156  orrabdioph  36157  rabren3dioph  36191  iunrelexp0  36807  dvradcnv2  37362  xpexb  37473  fsumcnf  37997  fprodcncf  38581  iblconstmpt  38641  itgiccshift  38666  itgperiod  38667  itgsbtaddcnst  38668  dirkercncflem2  38791  fourierdlem47  38840  sge0iunmpt  39105  sge0xaddlem2  39121  sge0xadd  39122  hoidmvlelem3  39281  ctvonmbl  39374  vonct  39378  smfaddlem2  39444  smfmullem4  39473  aoprssdm  39726  residfi  40157  uhgrstrrepelem  40295  usgrnbcnvfv  40585  ewlksfval  40795  crctcsh1wlkn0  41016  av-numclwwlk3lem  41530
  Copyright terms: Public domain W3C validator