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

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

Proof of Theorem eqeltrrdi
StepHypRef Expression
1 eqeltrrdi.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2830 . 2 (𝜑𝐴 = 𝐵)
3 eqeltrrdi.2 . 2 𝐵𝐶
42, 3eqeltrdi 2924 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896
This theorem is referenced by:  wemoiso2  7660  releldm2  7727  mapprc  8395  ixpprc  8468  bren  8503  brdomg  8504  domssex  8664  mapen  8667  ssenen  8677  fodomfib  8784  fi0  8870  dffi3  8881  brwdom  9017  brwdomn0  9019  unxpwdom2  9038  ixpiunwdom  9040  tcmin  9169  rankonid  9244  rankr1id  9277  cardf2  9358  cardid2  9368  carduni  9396  fseqen  9440  acndom  9464  acndom2  9467  alephnbtwn  9484  cardcf  9661  cfeq0  9665  cflim2  9672  coftr  9682  infpssr  9717  hsmexlem5  9839  axdc3lem4  9862  fodomb  9935  ondomon  9972  gruina  10227  ioof  12825  hashbc  13807  hashfacen  13808  trclun  14365  zsum  15066  fsum  15068  fprod  15286  eqgen  18324  symgfisg  18587  dvdsr  19387  asplss  20091  aspsubrg  20093  psrval  20130  clsf  21644  restco  21760  subbascn  21850  is2ndc  22042  ptbasin2  22174  ptbas  22175  indishmph  22394  ufldom  22558  cnextfres1  22664  ussid  22857  icopnfcld  23364  cnrehmeo  23549  csscld  23844  clsocv  23845  itg2gt0  24355  dvmptadd  24554  dvmptmul  24555  dvmptco  24566  logcn  25229  selberglem1  26120  hmopidmchi  29925  sigagensiga  31420  dya2iocbrsiga  31553  dya2icobrsiga  31554  logdivsqrle  31941  fnessref  33725  unirep  35056  indexdom  35077  dicfnN  38384  pwslnmlem0  39882  mendval  39974  icof  41704  dvsubf  42413  dvdivf  42421  itgsinexplem1  42453  stirlinglem7  42579  fourierdlem73  42678  fouriersw  42730  ovolval4lem1  43145
  Copyright terms: Public domain W3C validator