Theorem eqeltrrdi 2846

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 2742	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrrdi.2	. 2 ⊢ 𝐵 ∈ 𝐶
4	2, 3	eqeltrdi 2845	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-clel 2814

This theorem is referenced by:  axrep6g  5226  wemoiso2  7849  releldm2  7916  mapprc  8650  mapfoss  8671  ixpprc  8738  bren  8774  brenOLD  8775  brdomg  8777  brdomgOLD  8778  domssex  8963  mapen  8966  ssenen  8976  imafi  8996  fodomfib  9137  fi0  9223  dffi3  9234  brwdom  9370  brwdomn0  9372  unxpwdom2  9391  ixpiunwdom  9393  tcmin  9543  rankonid  9631  rankr1id  9664  cardf2  9745  cardid2  9755  carduni  9783  fseqen  9829  acndom  9853  acndom2  9856  alephnbtwn  9873  cardcf  10054  cfeq0  10058  cflim2  10065  coftr  10075  infpssr  10110  hsmexlem5  10232  axdc3lem4  10255  fodomb  10328  ondomon  10365  gruina  10620  ioof  13225  hashbc  14210  hashfacenOLD  14212  trclun  14770  zsum  15475  fsum  15477  fprod  15696  eqgen  18854  symgfisg  19121  dvdsr  19933  asplss  21123  aspsubrg  21125  psrval  21163  clsf  22244  restco  22360  subbascn  22450  is2ndc  22642  ptbasin2  22774  ptbas  22775  indishmph  22994  ufldom  23158  cnextfres1  23264  ussid  23457  icopnfcld  23976  cnrehmeo  24161  csscld  24458  clsocv  24459  itg2gt0  24970  dvmptadd  25169  dvmptmul  25170  dvmptco  25181  logcn  25847  selberglem1  26738  hmopidmchi  30558  sigagensiga  32154  dya2iocbrsiga  32287  dya2icobrsiga  32288  logdivsqrle  32675  fnessref  34591  unirep  35915  indexdom  35936  dicfnN  39239  pwslnmlem0  40954  mendval  41046  icof  42803  dvsubf  43504  dvdivf  43512  itgsinexplem1  43544  stirlinglem7  43670  fourierdlem73  43769  fouriersw  43821  ovolval4lem1  44237  i0oii  46271  io1ii  46272