Theorem eqeltrrdi 2838

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

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

This theorem is referenced by:  axrep6g  5248  snexg  5393  wemoiso2  7956  releldm2  8025  mapprc  8806  mapfoss  8828  ixpprc  8895  bren  8931  brdomg  8933  domssex  9108  mapen  9111  ssenen  9121  imafiOLD  9272  fodomfib  9287  fodomfibOLD  9289  fi0  9378  dffi3  9389  brwdom  9527  brwdomn0  9529  unxpwdom2  9548  ixpiunwdom  9550  tcmin  9701  rankonid  9789  rankr1id  9822  cardf2  9903  cardid2  9913  carduni  9941  fseqen  9987  acndom  10011  acndom2  10014  alephnbtwn  10031  cardcf  10212  cfeq0  10216  cflim2  10223  coftr  10233  infpssr  10268  hsmexlem5  10390  axdc3lem4  10413  fodomb  10486  ondomon  10523  gruina  10778  ioof  13415  hashbc  14425  trclun  14987  zsum  15691  fsum  15693  fprod  15914  eqgen  19120  symgfisg  19405  dvdsr  20278  asplss  21790  aspsubrg  21792  psrval  21831  clsf  22942  restco  23058  subbascn  23148  is2ndc  23340  ptbasin2  23472  ptbas  23473  indishmph  23692  ufldom  23856  cnextfres1  23962  ussid  24155  icopnfcld  24662  cnrehmeo  24858  cnrehmeoOLD  24859  csscld  25156  clsocv  25157  itg2gt0  25668  dvmptadd  25871  dvmptmul  25872  dvmptco  25883  logcn  26563  selberglem1  27463  noseq0  28191  hmopidmchi  32087  evl1deg2  33553  sigagensiga  34138  dya2iocbrsiga  34273  dya2icobrsiga  34274  logdivsqrle  34648  fnessref  36352  bj-snexg  37029  bj-unexg  37033  unirep  37715  indexdom  37735  dicfnN  41184  pwslnmlem0  43087  mendval  43175  orbitinit  44953  icof  45220  dvsubf  45919  dvdivf  45927  itgsinexplem1  45959  stirlinglem7  46085  fourierdlem73  46184  fouriersw  46236  ovolval4lem1  46654  lamberte  46896  i0oii  48912  io1ii  48913  2arwcatlem4  49591  2arwcat  49593