Theorem eqeltrrdi 2843

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  axrep6g  5294  snexg  5431  wemoiso2  7961  releldm2  8029  mapprc  8824  mapfoss  8846  ixpprc  8913  bren  8949  brenOLD  8950  brdomg  8952  brdomgOLD  8953  domssex  9138  mapen  9141  ssenen  9151  imafi  9175  fodomfib  9326  fi0  9415  dffi3  9426  brwdom  9562  brwdomn0  9564  unxpwdom2  9583  ixpiunwdom  9585  tcmin  9736  rankonid  9824  rankr1id  9857  cardf2  9938  cardid2  9948  carduni  9976  fseqen  10022  acndom  10046  acndom2  10049  alephnbtwn  10066  cardcf  10247  cfeq0  10251  cflim2  10258  coftr  10268  infpssr  10303  hsmexlem5  10425  axdc3lem4  10448  fodomb  10521  ondomon  10558  gruina  10813  ioof  13424  hashbc  14412  hashfacenOLD  14414  trclun  14961  zsum  15664  fsum  15666  fprod  15885  eqgen  19061  symgfisg  19336  dvdsr  20176  asplss  21428  aspsubrg  21430  psrval  21468  clsf  22552  restco  22668  subbascn  22758  is2ndc  22950  ptbasin2  23082  ptbas  23083  indishmph  23302  ufldom  23466  cnextfres1  23572  ussid  23765  icopnfcld  24284  cnrehmeo  24469  csscld  24766  clsocv  24767  itg2gt0  25278  dvmptadd  25477  dvmptmul  25478  dvmptco  25489  logcn  26155  selberglem1  27048  hmopidmchi  31404  sigagensiga  33139  dya2iocbrsiga  33274  dya2icobrsiga  33275  logdivsqrle  33662  gg-cnrehmeo  35171  fnessref  35242  bj-snexg  35915  bj-unexg  35919  unirep  36582  indexdom  36602  dicfnN  40054  pwslnmlem0  41833  mendval  41925  icof  43918  dvsubf  44630  dvdivf  44638  itgsinexplem1  44670  stirlinglem7  44796  fourierdlem73  44895  fouriersw  44947  ovolval4lem1  45365  i0oii  47552  io1ii  47553