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

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

Proof of Theorem eqeltrrid
StepHypRef Expression
1 eqeltrrid.1 . . 3 𝐵 = 𝐴
21eqcomi 2828 . 2 𝐴 = 𝐵
3 eqeltrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqeltrid 2915 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-clel 2891
This theorem is referenced by:  3eltr3g  2927  dmrnssfld  5834  oprssdm  7321  offval  7408  pwexr  7479  cnvexg  7621  resfunexgALT  7641  abrexexg  7654  abrexex2g  7657  opabex3d  7658  opabex3rd  7659  suppssov1  7854  suppssfv  7858  ralxpmap  8452  residfi  8797  imafi  8809  abrexfi  8816  ssfii  8875  wdomima2g  9042  unxpwdom2  9044  tskwe  9371  ac10ct  9452  fin23lem28  9754  fin23lem30  9756  axcclem  9871  distrlem4pr  10440  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  o1res  14909  exprmfct  16040  infpnlem1  16238  4sqlem13  16285  0ram  16348  ressval3d  16553  ismred2  16866  mreexexlem2d  16908  mreexexlem4d  16910  acsfn1c  16925  acsfn2  16926  ssclem  17081  submacs  17983  symgtset  18519  symgsubmefmndALT  18523  efgrcl  18833  cntrcmnd  18954  cntrabl  18955  dprd2da  19156  srgbinom  19287  irredlmul  19450  lidlrsppropd  19995  issubassa  20090  ply1crng  20358  ply1ring  20408  ply1lmod  20412  chrcl  20665  css1  20826  oftpos  21053  tposmap  21058  0opn  21504  fctop2  21605  difopn  21634  tgrest  21759  ordtbas2  21791  ordtopn3  21796  ordtcld3  21799  t1ficld  21927  resthauslem  21963  kgentopon  22138  txbasex  22166  txcnpi  22208  txdis1cn  22235  pthaus  22238  txkgen  22252  cnmptid  22261  cnmptc  22262  cnmpt1st  22268  cnmpt2nd  22269  cnmpt2c  22270  cnmptkc  22279  txconn  22289  hmeoima  22365  hmeocld  22367  xkohmeo  22415  filufint  22520  fin1aufil  22532  flftg  22596  ptcmplem2  22653  tmdmulg  22692  tmdgsum2  22696  submtmd  22704  symgtgp  22706  ghmcnp  22715  qustgpopn  22720  qustgplem  22721  ust0  22820  nrginvrcn  23293  fsumcn  23470  fsum2cn  23471  expcn  23472  cnheibor  23551  evth2  23556  csscld  23844  clsocv  23845  ovoliun2  24099  volfiniun  24140  dyadmbl  24193  mbfeqalem2  24235  mbfss  24239  ismbf3d  24247  mbfadd  24254  i1f0rn  24275  mbfmul  24319  itg2seq  24335  itg2monolem2  24344  itg2monolem3  24345  itg2mono  24346  itgreval  24389  itgge0  24403  itgss3  24407  iblconst  24410  itgconst  24411  ibladdlem  24412  itgfsum  24419  iblabslem  24420  itgabs  24427  lhop1lem  24602  dvfsumle  24610  dvfsumlem2  24616  ftc1lem4  24628  itgparts  24636  itgsubstlem  24637  itgsubst  24638  plydivlem1  24874  aannenlem1  24909  taylply2  24948  itgulm  24988  cxpcn  25318  resqrtcn  25322  basellem1  25650  mulogsumlem  26099  mulog2sumlem2  26103  selberg2lem  26118  pntrsumo1  26133  usgrnbcnvfv  27139  ewlksfval  27375  crctcshwlkn0  27591  pjssmii  29450  abrexexd  30261  pfxlsw2ccat  30619  cntrcrng  30690  ogrpaddltrbid  30714  lmatfval  31067  pl1cn  31186  esumcvg  31333  esumcvgsum  31335  sigaval  31358  sigaclfu2  31368  sigapildsys  31409  ldgenpisys  31413  measinb2  31470  braew  31489  unelcarsg  31558  carsgclctunlem2  31565  sibfof  31586  sitgclg  31588  orrvcoel  31711  orrvccel  31712  fsum2dsub  31866  subfaclefac  32411  cvmsss2  32509  cvmopnlem  32513  satf0suclem  32610  mpstrcl  32776  elmpps  32808  hmeoclda  33669  bj-1uplex  34308  bj-2uplex  34322  icoreclin  34620  broucube  34908  mblfinlem1  34911  cnambfre  34922  ibladdnclem  34930  iblabsnclem  34937  itgabsnc  34943  ftc1cnnclem  34947  ftc1anclem4  34952  ftc1anclem5  34953  ftc1anclem6  34954  ftc1anclem7  34955  ftc2nc  34958  areacirc  34969  zrdivrng  35213  xrnresex  35636  dalemrot  36775  dalem10  36791  arglem1N  37308  cdlemk36  38031  mzpconstmpt  39317  mzpresrename  39327  diophrex  39352  0dioph  39355  anrabdioph  39357  orrabdioph  39358  rabren3dioph  39392  iunrelexp0  40027  dvradcnv2  40659  xpexb  40766  fsumcnf  41258  uzublem  41683  fprodcncf  42163  iblconstmpt  42220  itgiccshift  42244  itgperiod  42245  itgsbtaddcnst  42246  dirkercncflem2  42369  fourierdlem47  42418  saluni  42589  sge0iunmpt  42680  sge0xaddlem2  42696  sge0xadd  42697  hoidmvlelem3  42859  ctvonmbl  42951  vonct  42955  smfaddlem2  43020  smfmullem4  43049  aoprssdm  43381
  Copyright terms: Public domain W3C validator