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

Theorem syl5eqelr 2735
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 2660 . 2 𝐴 = 𝐵
3 syl5eqelr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqel 2734 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:  3eltr3g  2746  dmrnssfld  5416  oprssdm  6857  offval  6946  pwexr  7016  cnvexg  7154  resfunexgALT  7171  abrexexg  7182  abrexex2g  7186  opabex3d  7187  suppssov1  7372  suppssfv  7376  ralxpmap  7949  residfi  8288  imafi  8300  abrexfi  8307  ssfii  8366  wdomima2g  8532  unxpwdom2  8534  tskwe  8814  ac10ct  8895  fin23lem28  9200  fin23lem30  9202  axcclem  9317  distrlem4pr  9886  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  o1res  14335  exprmfct  15463  infpnlem1  15661  4sqlem13  15708  0ram  15771  ressval3d  15984  ismred2  16310  mreexexlem2d  16352  mreexexlem4d  16354  acsfn1c  16370  acsfn2  16371  ssclem  16526  submacs  17412  efgrcl  18174  dprd2da  18487  srgbinom  18591  irredlmul  18754  lidlrsppropd  19278  issubassa  19372  ply1crng  19616  ply1ring  19666  ply1lmod  19670  chrcl  19922  css1  20082  oftpos  20306  tposmap  20311  0opn  20757  fctop2  20857  difopn  20886  tgrest  21011  ordtbas2  21043  ordtopn3  21048  ordtcld3  21051  t1ficld  21179  resthauslem  21215  kgentopon  21389  txbasex  21417  txcnpi  21459  txdis1cn  21486  pthaus  21489  txkgen  21503  cnmptid  21512  cnmptc  21513  cnmpt1st  21519  cnmpt2nd  21520  cnmpt2c  21521  cnmptkc  21530  txconn  21540  hmeoima  21616  hmeocld  21618  xkohmeo  21666  filufint  21771  fin1aufil  21783  flftg  21847  ptcmplem2  21904  tmdmulg  21943  tmdgsum2  21947  symgtgp  21952  submtmd  21955  ghmcnp  21965  qustgpopn  21970  qustgplem  21971  ust0  22070  nrginvrcn  22543  fsumcn  22720  fsum2cn  22721  expcn  22722  cnheibor  22801  evth2  22806  csscld  23094  clsocv  23095  ovoliun2  23320  volfiniun  23361  dyadmbl  23414  mbfeqalem  23454  mbfss  23458  ismbf3d  23466  mbfadd  23473  i1f0rn  23494  mbfmul  23538  itg2seq  23554  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itgreval  23608  itgge0  23622  itgss3  23626  iblconst  23629  itgconst  23630  ibladdlem  23631  itgfsum  23638  iblabslem  23639  itgabs  23646  mvth  23800  lhop1lem  23821  dvfsumle  23829  dvfsumlem2  23835  ftc1lem4  23847  itgparts  23855  itgsubstlem  23856  itgsubst  23857  plydivlem1  24093  aannenlem1  24128  taylply2  24167  itgulm  24207  cxpcn  24531  resqrtcn  24535  basellem1  24852  mulogsumlem  25265  mulog2sumlem2  25269  selberg2lem  25284  pntrsumo1  25299  usgrnbcnvfv  26311  ewlksfval  26553  crctcshwlkn0  26769  numclwwlk3lemOLD  27369  pjssmii  28668  abrexexd  29473  ogrpaddltrbid  29849  lmatfval  30008  pl1cn  30129  esumcvg  30276  esumcvgsum  30278  sigaval  30301  sigaclfu2  30312  sigapildsys  30353  ldgenpisys  30357  measinb2  30414  braew  30433  unelcarsg  30502  carsgclctunlem2  30509  sibfof  30530  sitgclg  30532  orrvcoel  30655  orrvccel  30656  fsum2dsub  30813  subfaclefac  31284  cvmsss2  31382  cvmopnlem  31386  mpstrcl  31564  elmpps  31596  hmeoclda  32453  bj-1uplex  33121  bj-2uplex  33135  bj-diagval  33220  icoreclin  33335  broucube  33573  mblfinlem1  33576  cnambfre  33588  ibladdnclem  33596  iblabsnclem  33603  itgabsnc  33609  ftc1cnnclem  33613  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc2nc  33624  areacirc  33635  zrdivrng  33882  xrnresex  34304  dalemrot  35261  dalem10  35277  arglem1N  35795  cdlemk36  36518  mzpconstmpt  37620  mzpresrename  37630  diophrex  37656  0dioph  37659  anrabdioph  37661  orrabdioph  37662  rabren3dioph  37696  iunrelexp0  38311  dvradcnv2  38863  xpexb  38975  fsumcnf  39494  uzublem  39970  fprodcncf  40432  iblconstmpt  40489  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  dirkercncflem2  40639  fourierdlem47  40688  saluni  40862  sge0iunmpt  40953  sge0xaddlem2  40969  sge0xadd  40970  hoidmvlelem3  41132  ctvonmbl  41224  vonct  41228  smfaddlem2  41293  smfmullem4  41322  aoprssdm  41603
  Copyright terms: Public domain W3C validator