Theorem eqeltrrdi 2870

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

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

This theorem is used by:  axrep6g  5243  snexgALT  5399  wemoiso2  7986  releldm2  8054  mapprc  8851  mapfoss  8874  ixpprc  8947  bren  8983  brdomg  8985  domssex  9157  mapen  9160  ssenen  9170  fodomfib  9320  fi0  9412  dffi3  9423  brwdom  9561  brwdomn0  9563  unxpwdom2  9582  ixpiunwdom  9584  tcmin  9740  rankonid  9839  rankr1id  9878  cardf2  10024  cardid2  10034  carduni  10062  fseqen  10106  acndom  10130  acndom2  10133  alephnbtwn  10150  cardcf  10329  cfeq0  10334  cflim2  10341  coftr  10351  infpssr  10386  hsmexlem5  10508  axdc3lem4  10531  fodomb  10605  ondomon  10647  gruina  10903  ioof  13578  hashbc  14598  trclun  15167  zsum  15884  fsum  15886  fprod  16108  eqgen  19393  symgfisg  19682  dvdsr  20592  asplss  22181  aspsubrg  22183  psrval  22223  clsf  23366  restco  23482  subbascn  23572  is2ndc  23764  ptbasin2  23897  ptbas  23898  indishmph  24117  ufldom  24281  cnextfres1  24387  ussid  24579  icopnfcld  25086  cnrehmeo  25274  csscld  25570  clsocv  25571  itg2gt0  26081  dvmptadd  26280  dvmptmul  26281  dvmptco  26292  logcn  26975  selberglem1  27872  noseq0  28676  hmopidmchi  32753  evl1deg2  34109  sigagensiga  34774  dya2iocbrsiga  34907  dya2icobrsiga  34908  logdivsqrle  35279  fnessref  37145  dfttc2g  37294  bj-snexg  37947  bj-unexg  37951  unirep  38648  indexdom  38668  dicfnN  42240  pwslnmlem0  44092  mendval  44180  orbitinit  45945  icof  46231  dvsubf  46923  dvdivf  46931  itgsinexplem1  46963  stirlinglem7  47089  fourierdlem73  47188  fouriersw  47240  ovolval4lem1  47658  lamberte  47937  i0oii  50027  io1ii  50028  2arwcatlem4  50705  2arwcat  50707