Theorem eqeltrrdi 2871

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  axrep6g  5240  snexgALT  5398  wemoiso2  7955  releldm2  8024  mapprc  8812  mapfoss  8833  ixpprc  8901  bren  8937  brdomg  8939  domssex  9110  mapen  9113  ssenen  9123  imafiOLD  9260  fodomfib  9273  fodomfibOLD  9274  fi0  9366  dffi3  9377  brwdom  9515  brwdomn0  9517  unxpwdom2  9536  ixpiunwdom  9538  tcmin  9694  rankonid  9787  rankr1id  9820  cardf2  9901  cardid2  9911  carduni  9939  fseqen  9983  acndom  10007  acndom2  10010  alephnbtwn  10027  cardcf  10208  cfeq0  10213  cflim2  10220  coftr  10230  infpssr  10265  hsmexlem5  10387  axdc3lem4  10410  fodomb  10483  ondomon  10520  gruina  10776  ioof  13451  hashbc  14466  trclun  15027  zsum  15745  fsum  15747  fprod  15971  eqgen  19222  symgfisg  19508  dvdsr  20411  asplss  21925  aspsubrg  21927  psrval  21967  clsf  23108  restco  23224  subbascn  23314  is2ndc  23506  ptbasin2  23638  ptbas  23639  indishmph  23858  ufldom  24022  cnextfres1  24128  ussid  24320  icopnfcld  24827  cnrehmeo  25015  csscld  25311  clsocv  25312  itg2gt0  25822  dvmptadd  26022  dvmptmul  26023  dvmptco  26034  logcn  26712  selberglem1  27609  noseq0  28383  hmopidmchi  32354  evl1deg2  33773  sigagensiga  34438  dya2iocbrsiga  34572  dya2icobrsiga  34573  logdivsqrle  34944  fnessref  36717  dfttc2g  36866  bj-snexg  37519  bj-unexg  37523  unirep  38213  indexdom  38233  dicfnN  41807  pwslnmlem0  43668  mendval  43756  orbitinit  45532  icof  45795  dvsubf  46488  dvdivf  46496  itgsinexplem1  46528  stirlinglem7  46654  fourierdlem73  46753  fouriersw  46805  ovolval4lem1  47223  lamberte  47482  i0oii  49541  io1ii  49542  2arwcatlem4  50219  2arwcat  50221