Theorem eqeltrrdi 2899

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  wemoiso2  7657  releldm2  7724  mapprc  8393  ixpprc  8466  bren  8501  brdomg  8502  domssex  8662  mapen  8665  ssenen  8675  fodomfib  8782  fi0  8868  dffi3  8879  brwdom  9015  brwdomn0  9017  unxpwdom2  9036  ixpiunwdom  9038  tcmin  9167  rankonid  9242  rankr1id  9275  cardf2  9356  cardid2  9366  carduni  9394  fseqen  9438  acndom  9462  acndom2  9465  alephnbtwn  9482  cardcf  9663  cfeq0  9667  cflim2  9674  coftr  9684  infpssr  9719  hsmexlem5  9841  axdc3lem4  9864  fodomb  9937  ondomon  9974  gruina  10229  ioof  12825  hashbc  13807  hashfacen  13808  trclun  14365  zsum  15067  fsum  15069  fprod  15287  eqgen  18325  symgfisg  18588  dvdsr  19392  asplss  20560  aspsubrg  20562  psrval  20600  clsf  21653  restco  21769  subbascn  21859  is2ndc  22051  ptbasin2  22183  ptbas  22184  indishmph  22403  ufldom  22567  cnextfres1  22673  ussid  22866  icopnfcld  23373  cnrehmeo  23558  csscld  23853  clsocv  23854  itg2gt0  24364  dvmptadd  24563  dvmptmul  24564  dvmptco  24575  logcn  25238  selberglem1  26129  hmopidmchi  29934  sigagensiga  31510  dya2iocbrsiga  31643  dya2icobrsiga  31644  logdivsqrle  32031  fnessref  33818  unirep  35151  indexdom  35172  dicfnN  38479  pwslnmlem0  40035  mendval  40127  icof  41848  dvsubf  42556  dvdivf  42564  itgsinexplem1  42596  stirlinglem7  42722  fourierdlem73  42821  fouriersw  42873  ovolval4lem1  43288