Theorem eqeltrrdi 2842

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

Step	Hyp	Ref	Expression
1		eqeltrrdi.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2738	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrrdi.2	. 2 ⊢ 𝐵 ∈ 𝐶
4	2, 3	eqeltrdi 2841	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  axrep6g  5293  snexg  5430  wemoiso2  7963  releldm2  8031  mapprc  8826  mapfoss  8848  ixpprc  8915  bren  8951  brenOLD  8952  brdomg  8954  brdomgOLD  8955  domssex  9140  mapen  9143  ssenen  9153  imafi  9177  fodomfib  9328  fi0  9417  dffi3  9428  brwdom  9564  brwdomn0  9566  unxpwdom2  9585  ixpiunwdom  9587  tcmin  9738  rankonid  9826  rankr1id  9859  cardf2  9940  cardid2  9950  carduni  9978  fseqen  10024  acndom  10048  acndom2  10051  alephnbtwn  10068  cardcf  10249  cfeq0  10253  cflim2  10260  coftr  10270  infpssr  10305  hsmexlem5  10427  axdc3lem4  10450  fodomb  10523  ondomon  10560  gruina  10815  ioof  13426  hashbc  14414  hashfacenOLD  14416  trclun  14963  zsum  15666  fsum  15668  fprod  15887  eqgen  19063  symgfisg  19338  dvdsr  20180  asplss  21434  aspsubrg  21436  psrval  21474  clsf  22559  restco  22675  subbascn  22765  is2ndc  22957  ptbasin2  23089  ptbas  23090  indishmph  23309  ufldom  23473  cnextfres1  23579  ussid  23772  icopnfcld  24291  cnrehmeo  24476  csscld  24773  clsocv  24774  itg2gt0  25285  dvmptadd  25484  dvmptmul  25485  dvmptco  25496  logcn  26162  selberglem1  27055  hmopidmchi  31442  sigagensiga  33208  dya2iocbrsiga  33343  dya2icobrsiga  33344  logdivsqrle  33731  gg-cnrehmeo  35240  fnessref  35328  bj-snexg  36001  bj-unexg  36005  unirep  36668  indexdom  36688  dicfnN  40140  pwslnmlem0  41915  mendval  42007  icof  43997  dvsubf  44709  dvdivf  44717  itgsinexplem1  44749  stirlinglem7  44875  fourierdlem73  44974  fouriersw  45026  ovolval4lem1  45444  i0oii  47630  io1ii  47631