Theorem eqeltrrdi 2837

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  axrep6g  5229  snexg  5374  wemoiso2  7909  releldm2  7978  mapprc  8757  mapfoss  8779  ixpprc  8846  bren  8882  brdomg  8884  domssex  9055  mapen  9058  ssenen  9068  imafiOLD  9205  fodomfib  9219  fodomfibOLD  9221  fi0  9310  dffi3  9321  brwdom  9459  brwdomn0  9461  unxpwdom2  9480  ixpiunwdom  9482  tcmin  9637  rankonid  9725  rankr1id  9758  cardf2  9839  cardid2  9849  carduni  9877  fseqen  9921  acndom  9945  acndom2  9948  alephnbtwn  9965  cardcf  10146  cfeq0  10150  cflim2  10157  coftr  10167  infpssr  10202  hsmexlem5  10324  axdc3lem4  10347  fodomb  10420  ondomon  10457  gruina  10712  ioof  13350  hashbc  14360  trclun  14921  zsum  15625  fsum  15627  fprod  15848  eqgen  19060  symgfisg  19347  dvdsr  20247  asplss  21781  aspsubrg  21783  psrval  21822  clsf  22933  restco  23049  subbascn  23139  is2ndc  23331  ptbasin2  23463  ptbas  23464  indishmph  23683  ufldom  23847  cnextfres1  23953  ussid  24146  icopnfcld  24653  cnrehmeo  24849  cnrehmeoOLD  24850  csscld  25147  clsocv  25148  itg2gt0  25659  dvmptadd  25862  dvmptmul  25863  dvmptco  25874  logcn  26554  selberglem1  27454  noseq0  28189  hmopidmchi  32095  evl1deg2  33513  sigagensiga  34114  dya2iocbrsiga  34249  dya2icobrsiga  34250  logdivsqrle  34624  fnessref  36341  bj-snexg  37018  bj-unexg  37022  unirep  37704  indexdom  37724  dicfnN  41172  pwslnmlem0  43074  mendval  43162  orbitinit  44940  icof  45207  dvsubf  45905  dvdivf  45913  itgsinexplem1  45945  stirlinglem7  46071  fourierdlem73  46170  fouriersw  46222  ovolval4lem1  46640  lamberte  46882  i0oii  48914  io1ii  48915  2arwcatlem4  49593  2arwcat  49595