Theorem eqeltrrdi 2845

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 2844	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  axrep6g  5235  snexg  5380  wemoiso2  7918  releldm2  7987  mapprc  8769  mapfoss  8791  ixpprc  8859  bren  8895  brdomg  8897  domssex  9068  mapen  9071  ssenen  9081  imafiOLD  9218  fodomfib  9231  fodomfibOLD  9233  fi0  9325  dffi3  9336  brwdom  9474  brwdomn0  9476  unxpwdom2  9495  ixpiunwdom  9497  tcmin  9650  rankonid  9743  rankr1id  9776  cardf2  9857  cardid2  9867  carduni  9895  fseqen  9939  acndom  9963  acndom2  9966  alephnbtwn  9983  cardcf  10164  cfeq0  10168  cflim2  10175  coftr  10185  infpssr  10220  hsmexlem5  10342  axdc3lem4  10365  fodomb  10438  ondomon  10475  gruina  10731  ioof  13365  hashbc  14378  trclun  14939  zsum  15643  fsum  15645  fprod  15866  eqgen  19112  symgfisg  19399  dvdsr  20300  asplss  21831  aspsubrg  21833  psrval  21873  clsf  22994  restco  23110  subbascn  23200  is2ndc  23392  ptbasin2  23524  ptbas  23525  indishmph  23744  ufldom  23908  cnextfres1  24014  ussid  24206  icopnfcld  24713  cnrehmeo  24909  cnrehmeoOLD  24910  csscld  25207  clsocv  25208  itg2gt0  25719  dvmptadd  25922  dvmptmul  25923  dvmptco  25934  logcn  26614  selberglem1  27514  noseq0  28288  hmopidmchi  32228  evl1deg2  33660  sigagensiga  34300  dya2iocbrsiga  34434  dya2icobrsiga  34435  logdivsqrle  34809  fnessref  36553  bj-snexg  37237  bj-unexg  37241  unirep  37917  indexdom  37937  dicfnN  41465  pwslnmlem0  43354  mendval  43442  orbitinit  45218  icof  45484  dvsubf  46179  dvdivf  46187  itgsinexplem1  46219  stirlinglem7  46345  fourierdlem73  46444  fouriersw  46496  ovolval4lem1  46914  lamberte  47155  i0oii  49186  io1ii  49187  2arwcatlem4  49864  2arwcat  49866