Theorem eqeltrrdi 2869

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  axrep6g  5245  snexgALT  5406  wemoiso2  7972  releldm2  8041  mapprc  8833  mapfoss  8856  ixpprc  8929  bren  8965  brdomg  8967  domssex  9139  mapen  9142  ssenen  9152  fodomfib  9301  fi0  9393  dffi3  9404  brwdom  9542  brwdomn0  9544  unxpwdom2  9563  ixpiunwdom  9565  tcmin  9721  rankonid  9814  rankr1id  9847  cardf2  9951  cardid2  9961  carduni  9989  fseqen  10033  acndom  10057  acndom2  10060  alephnbtwn  10077  cardcf  10256  cfeq0  10261  cflim2  10268  coftr  10278  infpssr  10313  hsmexlem5  10435  axdc3lem4  10458  fodomb  10532  ondomon  10574  gruina  10830  ioof  13503  hashbc  14521  trclun  15090  zsum  15807  fsum  15809  fprod  16031  eqgen  19309  symgfisg  19598  dvdsr  20506  asplss  22091  aspsubrg  22093  psrval  22133  clsf  23276  restco  23392  subbascn  23482  is2ndc  23674  ptbasin2  23807  ptbas  23808  indishmph  24027  ufldom  24191  cnextfres1  24297  ussid  24489  icopnfcld  24996  cnrehmeo  25184  csscld  25480  clsocv  25481  itg2gt0  25991  dvmptadd  26190  dvmptmul  26191  dvmptco  26202  logcn  26887  selberglem1  27784  noseq0  28558  hmopidmchi  32635  evl1deg2  33990  sigagensiga  34655  dya2iocbrsiga  34789  dya2icobrsiga  34790  logdivsqrle  35161  fnessref  36979  dfttc2g  37128  bj-snexg  37781  bj-unexg  37785  unirep  38467  indexdom  38487  dicfnN  42059  pwslnmlem0  43935  mendval  44023  orbitinit  45782  icof  46052  dvsubf  46745  dvdivf  46753  itgsinexplem1  46785  stirlinglem7  46911  fourierdlem73  47010  fouriersw  47062  ovolval4lem1  47480  lamberte  47759  i0oii  49849  io1ii  49850  2arwcatlem4  50527  2arwcat  50529