Theorem eqeltrrdi 2834

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-clel 2802

This theorem is referenced by:  axrep6g  5284  snexg  5421  wemoiso2  7955  releldm2  8023  mapprc  8821  mapfoss  8843  ixpprc  8910  bren  8946  brenOLD  8947  brdomg  8949  brdomgOLD  8950  domssex  9135  mapen  9138  ssenen  9148  imafi  9172  fodomfib  9323  fi0  9412  dffi3  9423  brwdom  9559  brwdomn0  9561  unxpwdom2  9580  ixpiunwdom  9582  tcmin  9733  rankonid  9821  rankr1id  9854  cardf2  9935  cardid2  9945  carduni  9973  fseqen  10019  acndom  10043  acndom2  10046  alephnbtwn  10063  cardcf  10244  cfeq0  10248  cflim2  10255  coftr  10265  infpssr  10300  hsmexlem5  10422  axdc3lem4  10445  fodomb  10518  ondomon  10555  gruina  10810  ioof  13422  hashbc  14410  hashfacenOLD  14412  trclun  14959  zsum  15662  fsum  15664  fprod  15883  eqgen  19100  symgfisg  19380  dvdsr  20256  asplss  21738  aspsubrg  21740  psrval  21779  clsf  22876  restco  22992  subbascn  23082  is2ndc  23274  ptbasin2  23406  ptbas  23407  indishmph  23626  ufldom  23790  cnextfres1  23896  ussid  24089  icopnfcld  24608  cnrehmeo  24802  cnrehmeoOLD  24803  csscld  25101  clsocv  25102  itg2gt0  25614  dvmptadd  25816  dvmptmul  25817  dvmptco  25828  logcn  26500  selberglem1  27397  noseq0  28082  hmopidmchi  31876  sigagensiga  33631  dya2iocbrsiga  33766  dya2icobrsiga  33767  logdivsqrle  34153  fnessref  35733  bj-snexg  36406  bj-unexg  36410  unirep  37076  indexdom  37096  dicfnN  40548  pwslnmlem0  42347  mendval  42439  icof  44428  dvsubf  45140  dvdivf  45148  itgsinexplem1  45180  stirlinglem7  45306  fourierdlem73  45405  fouriersw  45457  ovolval4lem1  45875  i0oii  47764  io1ii  47765