Theorem eqeltrrdi 2840

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  axrep6g  5226  snexg  5371  wemoiso2  7906  releldm2  7975  mapprc  8754  mapfoss  8776  ixpprc  8843  bren  8879  brdomg  8881  domssex  9051  mapen  9054  ssenen  9064  imafiOLD  9200  fodomfib  9213  fodomfibOLD  9215  fi0  9304  dffi3  9315  brwdom  9453  brwdomn0  9455  unxpwdom2  9474  ixpiunwdom  9476  tcmin  9629  rankonid  9722  rankr1id  9755  cardf2  9836  cardid2  9846  carduni  9874  fseqen  9918  acndom  9942  acndom2  9945  alephnbtwn  9962  cardcf  10143  cfeq0  10147  cflim2  10154  coftr  10164  infpssr  10199  hsmexlem5  10321  axdc3lem4  10344  fodomb  10417  ondomon  10454  gruina  10709  ioof  13347  hashbc  14360  trclun  14921  zsum  15625  fsum  15627  fprod  15848  eqgen  19093  symgfisg  19380  dvdsr  20280  asplss  21811  aspsubrg  21813  psrval  21852  clsf  22963  restco  23079  subbascn  23169  is2ndc  23361  ptbasin2  23493  ptbas  23494  indishmph  23713  ufldom  23877  cnextfres1  23983  ussid  24175  icopnfcld  24682  cnrehmeo  24878  cnrehmeoOLD  24879  csscld  25176  clsocv  25177  itg2gt0  25688  dvmptadd  25891  dvmptmul  25892  dvmptco  25903  logcn  26583  selberglem1  27483  noseq0  28220  hmopidmchi  32131  evl1deg2  33540  sigagensiga  34154  dya2iocbrsiga  34288  dya2icobrsiga  34289  logdivsqrle  34663  fnessref  36401  bj-snexg  37078  bj-unexg  37082  unirep  37764  indexdom  37784  dicfnN  41292  pwslnmlem0  43194  mendval  43282  orbitinit  45059  icof  45326  dvsubf  46022  dvdivf  46030  itgsinexplem1  46062  stirlinglem7  46188  fourierdlem73  46287  fouriersw  46339  ovolval4lem1  46757  lamberte  46998  i0oii  49030  io1ii  49031  2arwcatlem4  49709  2arwcat  49711