Theorem eqeltrrdi 2849

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-clel 2817

This theorem is referenced by:  wemoiso2  7803  releldm2  7870  mapprc  8593  mapfoss  8614  ixpprc  8681  bren  8717  brenOLD  8718  brdomg  8719  domssex  8890  mapen  8893  ssenen  8903  imafi  8923  fodomfib  9054  fi0  9140  dffi3  9151  brwdom  9287  brwdomn0  9289  unxpwdom2  9308  ixpiunwdom  9310  tcmin  9482  rankonid  9571  rankr1id  9604  cardf2  9685  cardid2  9695  carduni  9723  fseqen  9767  acndom  9791  acndom2  9794  alephnbtwn  9811  cardcf  9992  cfeq0  9996  cflim2  10003  coftr  10013  infpssr  10048  hsmexlem5  10170  axdc3lem4  10193  fodomb  10266  ondomon  10303  gruina  10558  ioof  13161  hashbc  14146  hashfacenOLD  14148  trclun  14706  zsum  15411  fsum  15413  fprod  15632  eqgen  18790  symgfisg  19057  dvdsr  19869  asplss  21059  aspsubrg  21061  psrval  21099  clsf  22180  restco  22296  subbascn  22386  is2ndc  22578  ptbasin2  22710  ptbas  22711  indishmph  22930  ufldom  23094  cnextfres1  23200  ussid  23393  icopnfcld  23912  cnrehmeo  24097  csscld  24394  clsocv  24395  itg2gt0  24906  dvmptadd  25105  dvmptmul  25106  dvmptco  25117  logcn  25783  selberglem1  26674  hmopidmchi  30492  sigagensiga  32088  dya2iocbrsiga  32221  dya2icobrsiga  32222  logdivsqrle  32609  fnessref  34525  unirep  35850  indexdom  35871  dicfnN  39176  pwslnmlem0  40896  mendval  40988  icof  42712  dvsubf  43409  dvdivf  43417  itgsinexplem1  43449  stirlinglem7  43575  fourierdlem73  43674  fouriersw  43726  ovolval4lem1  44141  i0oii  46165  io1ii  46166